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).
Last updated: Aug 13 2022 at 07:19 UTC