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).


Last updated: Aug 13 2022 at 07:19 UTC