*To*: Lars-Henrik Eriksson <lhe at it.uu.se>*Subject*: Re: [isabelle] Problem with "additional type variables" in a definition*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*Date*: Tue, 24 May 2016 10:09:44 +0000*Accept-language*: de-DE, de-AT, en-US*Cc*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <58B252C5-05D9-4412-B0DC-CD97FF5B1C36@it.uu.se>*References*: <58B252C5-05D9-4412-B0DC-CD97FF5B1C36@it.uu.se>*Thread-index*: AQHRtaAvY5oe2uRhcUahtMbMvqRppJ/HvACA*Thread-topic*: [isabelle] Problem with "additional type variables" in a definition

Dear Lars-Henrik, > I'm having a problem with Isabelle 2016 which I've minimised to the following file. There seems to be something particular in how Isabelle handles types appearing in a definition but not in any arguments to the thing being defined. > > theory Test > imports > HOL > begin > > definition foo :: "bool" ("f" 50) where > "foo â âx :: 'a. True" > > abbreviation bar :: "bool" where > "bar â foo" > > lemma "foo" > sorry > end > > The definition gives the output > > consts > foo :: "bool" > Additional type variable(s) in specification of "foo": âa The problem is the implicit type âa in the definition of foo. To this end, Isabelle inserts a dummy argument in the definition of foo of type (âa itself). So your definition becomes definition foo' :: "'a itself â bool" where "foo' _ â â x :: 'a. Trueâ you also see this definition, if you perform a âprint_theoremsâ after your definition of âfooâ. Hope this helps, RenÃ

**Follow-Ups**:**Re: [isabelle] Problem with "additional type variables" in a definition***From:*Lars-Henrik Eriksson

**References**:**[isabelle] Problem with "additional type variables" in a definition***From:*Lars-Henrik Eriksson

- Previous by Date: Re: [isabelle] Isabelle/HOL 2005
- Next by Date: Re: [isabelle] Isabelle 2005 request
- Previous by Thread: [isabelle] Problem with "additional type variables" in a definition
- Next by Thread: Re: [isabelle] Problem with "additional type variables" in a definition
- Cl-isabelle-users May 2016 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