Stream: Beginner Questions

Topic: Malformed global fact: illegal fixed variable

view this post on Zulip Lukas Stevens (May 03 2022 at 08:50):

Is anyone familiar with the error message:

Malformed global fact "Set_Proc.open_branch.lemma_3_1"⌂
Illegal fixed variable: "'a"

view this post on Zulip Lukas Stevens (May 03 2022 at 09:04):

Even for

lemma foo: "True" by auto

I get this error message. The message occurs as soon as I give the lemma a name.

view this post on Zulip Lukas Stevens (May 03 2022 at 09:06):

The problem occurs only after a sublocale in the locale open_branch.

view this post on Zulip Lukas Stevens (May 03 2022 at 09:09):

Ah, I tracked down the error. It was because I didn't fully instantiate the sublocale (one argument was missing).

view this post on Zulip Alexander Schlenga (Sep 13 2023 at 12:40):

Thanks, that helped me solving the same issue!

Last updated: Apr 26 2024 at 04:17 UTC