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.


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 - 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.