Re: [isabelle] Loose bound variable
I wanted to prove a lemma with an apply script. After some
manipulations (induct, rule, drule, frule) of the goals, auto,
fastsimp or force should easily solve the remaining goal. However,
simp (and all methods that use the simplifier) produce only this
*** exception TYPE raised (line 341 of "sign.ML"): Loose bound
*** At command "apply".
What does this error message mean?
Isabelle's internal representation of lambda-terms uses de Bruijn
indices for bound variables. Errors like these usually mean that
there's a rather bad bug in some code that directly manipulates term
(e.g., some code that removes a lambda abstraction forgot to decrement
te bound variable indices).
And how can I avoid it? Is there something wrong with my simplifier
Is there anything _special_ about your simplifier setup?
This archive was generated by a fusion of
Pipermail (Mailman edition) and