Is anyone familiar with the error message:
Malformed global fact "Set_Proc.open_branch.lemma_3_1"⌂ Illegal fixed variable: "'a"
lemma foo: "True" by auto
I get this error message. The message occurs as soon as I give the lemma a name.
The problem occurs only after a sublocale in the locale
Ah, I tracked down the error. It was because I didn't fully instantiate the sublocale (one argument was missing).
Thanks, that helped me solving the same issue!
Last updated: Dec 07 2023 at 20:16 UTC