Lukas Stevens (May 03 2022 at 08:50): 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"
Even for
lemma foo: "True" by auto
I get this error message. The message occurs as soon as I give the lemma a name.
Lukas Stevens (May 03 2022 at 09:06):The problem occurs only after a sublocale in the locale open_branch.
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).
Alexander Schlenga (Sep 13 2023 at 12:40):Thanks, that helped me solving the same issue!
Last updated: Dec 21 2024 at 16:20 UTC