Yiming Xu (Sep 12 2024 at 18:15): Yiming Xu (Sep 12 2024 at 18:15):
Yiming Xu (Sep 12 2024 at 18:16):I am working on an induction and the inductive case gives a free variable with name "fa__".
Mathias Fleury (Sep 12 2024 at 18:17):then name it
Yiming Xu (Sep 12 2024 at 18:17):But when I copy and paste the name and want to prove a fact about it, Isabelle complains about the bad name.
Mathias Fleury (Sep 12 2024 at 18:17):that what the case is for
Mathias Fleury (Sep 12 2024 at 18:18):case (3 p f a g)
Yiming Xu (Sep 12 2024 at 18:19):Thank you, the world is peaceful again. So it is just because it is unhappy with names with "_"?
Mathias Fleury (Sep 12 2024 at 18:19):these are internal names you are not supposed to use
Yiming Xu (Sep 12 2024 at 18:21):Got it. I am a bit suprised because I can type things like "?case" with these question mark.
Last updated: Dec 21 2024 at 16:20 UTC