Re: [isabelle] Code equations for UNION in Isabelle2012-RC1



Hi Andreas,


> For example, of the following abbreviations, x y and z work, although
> they specialize types, but u does not. What is the fundamental difference?
> 
> abbreviation x :: nat where "x == 0" (* overloaded constant *)
> abbreviation y :: "nat => nat => nat" where "y == op +" (* overloaded
> operator *)
> abbreviation z :: "nat => nat => nat" where "z == power" (* definition
> in type class *)
> abbreviation u :: "(nat => bool) => nat" where "u == Least"

For me (rev. ca5b629a5995), z does not work either.

The argument list given to export_code is parsed as a list of terms, so
abbreviations are expanded.  The result is then checked to be a constant
of an appropriate type with implicit monomorphization of class
operations (cf. Code.read_const).  In your example, x and y are such
instances of class operations;  z and u are not but parametricly
polymorphic (although dependent on a class operation wrt. to the
underlying code equations) and thus need to be specified with their
general type.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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