*To*: cl-isabelle-users at lists.cam.ac.uk, Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Code equations for UNION in Isabelle2012-RC1*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sun, 13 May 2012 10:03:23 +0200*In-reply-to*: <4FA76E5B.1090309@kit.edu>*Organization*: TU Munich*References*: <4FA3D9D1.6010701@kit.edu> <4FA3E59F.6040909@informatik.tu-muenchen.de> <4FA76E5B.1090309@kit.edu>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:12.0) Gecko/20120430 Thunderbird/12.0.1

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**

**References**:**[isabelle] Code equations for UNION in Isabelle2012-RC1***From:*Andreas Lochbihler

**Re: [isabelle] Code equations for UNION in Isabelle2012-RC1***From:*Florian Haftmann

**Re: [isabelle] Code equations for UNION in Isabelle2012-RC1***From:*Andreas Lochbihler

- Previous by Date: [isabelle] "isabelle make" in windows-RC2
- Next by Date: Re: [isabelle] Isabelle on OpenBSD?
- Previous by Thread: Re: [isabelle] Code equations for UNION in Isabelle2012-RC1
- Next by Thread: [isabelle] Proof help on Cardinality and list_all2
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list