Re: [isabelle] Loose bound variable



Hi Jasmin,

thank you for the explanation.

*** 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?
No, not really. I have added some lemmas to the simp set, but that's about all. In particular, I haven't written any simpprocs.

If you like, I can send you my Isabelle2009-1/HOL theories such that you can reproduce the error and try to find bug.

Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft





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