Re: [isabelle] HOLCF equality



On Sat, Jul 7, 2012 at 6:04 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
> Dear all,
>
> is there already something like Haskell's "Eq" typeclass for HOLCF (which
> seems to be neccessariy/convenient to formalize typical Haskell functions).
> If not, are there any other reasons than lack of time?

A library with class "Eq" and other classes from Haskell would
certainly be useful, and I don't think it would take much time to
implement.

I think the main reason I never implemented it is I could never decide
on the details: what to name the functions, what syntax to provide,
what axioms to use, which classes to provide, etc.

- Brian





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