Email Gateway (Aug 17 2022 at 13:26): Email Gateway (Aug 17 2022 at 13:26):From: Cary Kempston <cdjk@cs.stanford.edu>
Is it possible to use numbers in variable names? I thought it was,
but then ran into a problem shown in the theory below. It seems like
it should work, unless I don't understand something...
theory Scratch = Main:
a TestLetter: "x --> x"
by (simp)
lemma TestNumber: "x1 --> x1"
by (simp)
lemmas LetterNew = TestLetter [where x="a & b"]
thm LetterNew
(* this doesn't work *)
lemmas NumberNew = TestNumber [where x1="a & b"]
thm NumberNew
end
Email Gateway (Aug 17 2022 at 13:26):From: nipkow@in.tum.de
(* this doesn't work *)
lemmas NumberNew = TestNumber [where x1="a & b"]
This works:
lemmas NumberNew = TestNumber [where ?x1.0="a & b"]
?-Vars are internally indexed. If the variable name ends in a number the
index must be given explicitly to avoid ambiguity.
Tobias
Last updated: May 03 2024 at 04:19 UTC