Re: [isabelle] instance theorems
What exactly does this strange allusion to a ``bug in Isabelle''
the bottom of p. 8?
If there are no bugs in Isabelle, the instance theorems will be
correctly. This is all. I suppose that holds for all of what I am
I didn't think to write that. I do not think that there is a bug in
The allusion was meant to distinguish between the lack of possibility
of programmer error (barring an Isabelle bug) in the elaboration
the strong potential for user error in the use phase.
Anyway, you have all theses consts as part of axclass/instance. From
where did you get these? Note that the purely logical concept of
axiomatic type classes cannot express such membership.
But I have access to not only the type class definitions, but the
constant definitions as well.
The only problem is matching undefined constants such as <= to
their type class. As the class is usually explicit, this is not
a problem. For instance, from <= : 'a:: ord -> 'a -> bool it is
easy to figure where to put this constant.
Also, most axiomatic type classes have axioms, which contain constants
on which the axioms hold. If these constants are not defined, then
they are in the list. So if order were defined without ord,
<= would be the list, but Least not.
This archive was generated by a fusion of
Pipermail (Mailman edition) and