Email Gateway (Aug 18 2022 at 13:54): Email Gateway (Aug 18 2022 at 13:54):From: Randy Pollack <rpollack@inf.ed.ac.uk>
The Isabelle parser is a mystery to me, and I am not very careful
about precedences, preferring to add a few parentheses when needed.
But I am stuck on a parsing problem now (using standard Isabelle
2009). The problem appears in a big development, not in simple
extracted form. Take a look at the error message before I ship you
many files.
inductive
"Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" ( "_ xxxxx _" )
where
b1[intro]: "t1 xxxxx t2 \<Longrightarrow> (App t1 s) xxxxx (App t2 s)"
| b2[intro]: "s1 xxxxx s2 \<Longrightarrow> (App t s1) xxxxx (App t s2)"
| b3[intro]: "t1 xxxxx t2 \<Longrightarrow> (Lam [X].t1) xxxxx (Lam [X].t2)"
| b4[intro]: "(App (Lam [X].t) s) xxxxx (t[X::=s])"
term "(s::lam) xxxxx (t::lam)"
The error message is
### Ambiguous input
### produces 2 parse trees:
### ("\<^const>local.Beta" ("_constrain" s lam) ("_constrain" t lam))
### ("\<^const>lam_bbS_thy.H.Beta" ("_constrain" s lam) ("_constrain" t lam))
*** Ambiguous input, 2 terms are type correct:
*** (s\<Colon>lam) xxxxx (t\<Colon>lam)
*** (s\<Colon>lam) xxxxx (t\<Colon>lam)
*** Failed to parse term
*** At command "term".
I've included type annotations, and there is nothing to parenthesize
for disambiguation. Neither the identifier "Beta" nor the identifier
"xxxxx" appear in the development before this point. I am using
several locales. "lam_bbS_thy" is the name of the file/theory in
which this occurs; this string is not used as an identifier inside the
theory. I have no idea what "H" is about; the identifier "H" does not
appear anywhere in the file "lam_bbS_thy", but I do have an identifier
"H" in previous files.
Any ideas, or do you need the whole development?
Thanks,
Randy
Last updated: Nov 21 2024 at 12:39 UTC