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.


	Makarius





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