Re: [isabelle] Porting trouble: Interpretation of locale semiring_1

Quoting Peter Lammich <peter.lammich at>:

I'm currently converting theories from 2008 -> 2009:


*** Partially applied constant on left hand side of equation
*** "semiring_1.of_nat {[]} {} op \<union> ?n \<equiv>
semiring_1.of_nat_aux (\<lambda>i. i \<union> {[]}) ?n {}"
*** At command "done".

I do not know what this error message means, nor can I find any
In Isabelle2008, the proof worked well.

This error is generated by the code generator (while processing the
interpreted lemmas).  It is apparently unable to deal with the
equation generated by the interpretation.

I only partially agree with Florian that interpretation doesn't do the right thing for definitions. It is important to note that interpretation must always give the user the freedom to map defined concepts to what he or she wants, not something the code generator is willing to accept. This also applies to locales generated via the class commands. Getting it right once and for all for the code generator seems to me like introducing a serious design flaw to interpretation.


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