Re: [isabelle] Loose bound variable

Hi Andreas,

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 error message:

*** exception TYPE raised (line 341 of "sign.ML"): Loose bound variable: B.4
*** 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 setup?

Is there anything _special_ about your simplifier setup?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.