Re: [isabelle] HOLCF
On Wed, 27 Jun 2012, Christian Sternagel wrote:
* definitions do not allow "natural" equations like "f$x$y = P x y", we have
to use "f = Lambda x y. P x y" instead.
In principle the 'definition' package has a filter to convert between the
specification given by the user, and the actual definition of the strict
form "f == RHS". It is rather simplistic, though, so it can probably not
be stretched that far.
How about non-recursive 'fixrec'? That would be analogous to using 'fun'
in HOL to get pattern matching, instead of trying to add this
functionality to the basic 'definition' package.
This archive was generated by a fusion of
Pipermail (Mailman edition) and