Re: [isabelle] malformed dependency




Isabelle's check for non-circularity of overloaded definitions restricts
checked overloaded definitions to overloading patterns similiar to what
is possible in Haskell 1.0; if this is not enough and you trust your
definitions not to introduce inconsistencies (by a suitable meta-proof),
you may turn the check of by writing

defs (unchecked)

instead of

defs (overloaded)
As Florian states in the above, when using defs(unchecked), you are on your own; especially, your definitions are just axioms then, which you have to trust, and which might introduce inconsistencies.

In order to circumvent this problem, you can use together with defs(unchecked) my package for checking overloaded definitions. It is more powerful than the built-in test of Isabelle and might be able to prove the consistency of your definitions (and it also tells you when your definitions are definitely circular and such). You can find it at http://www4.in.tum.de/~obua/checkdefs. Don't hesitate to ask me if you have more questions,

Steven





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