exception TYPE raised (line XXX of "envir.ML"): expand_atom: ill-typed replacement
This error can occur if you bind and use a pattern in a lemma statement, e.g.
lemma assumes "P foo" (is "P ?bar") shows "Q ?bar"
This is due to the fact that parsing and type inference for the whole lemma statement is done at once.
Fix: Sufficiently verbose type annotations might help, e.g.
lemma assumes "P (foo ::'a)" (is "P ?bar") shows "Q (?bar :: 'a)"
Bad Name: "t :: T"
When typing a definition and using type annotations at the wrong position, as in:
definition "a :: bool" where "a ≡ False"
Bad name: "a :: bool".
Fix: use type annotations in the
where clause instead:
definition "a" where "a :: bool ≡ False"
Not an equation | Not a meta-equality (≡)
Most commonly, these errors occur because Isabelle's equality
= binds relatively strongly.
definition d where "d b = b ∧ False" fun f where "f b = b ∧ False"
lead both to above error.
Isabelle parses the term
t b = b ∧ False as
(t b = b) ∧ False and not
t b = (b ∧ False).
Explicitly set the parentheses, e.g.
t b = (b ∧ False)