*To*: Nicole Rauch <rauch at informatik.uni-kl.de>*Subject*: Re: [isabelle] Extra type variables in constdef*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 21 Sep 2007 10:44:03 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <D83FEB81-38AA-44DA-A5D0-43BD1005E9CC@informatik.uni-kl.de>*References*: <D83FEB81-38AA-44DA-A5D0-43BD1005E9CC@informatik.uni-kl.de>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

Tobias Nicole Rauch wrote:

Dear all,I'm having trouble getting rid of extra type variables that appear onthe right-hand side of a constant definition. This is my setting:axclass someAxClass < type consts a :: "int => ('a::someAxClass)" b :: "('a::someAxClass) => bool" Now if I define a constant that groups together these two consts, say constdefs c :: "int => bool" "c x == b (a x)" I get the error message *** Specification depends on extra type variables: "'a"Is there any way to work around this, e.g. can c depend on 'a (similarto polymorphic datatype declarations) ?Or is my attempt generally considered bad design and should beformalized differently?Thanks for any insights Nicole Rauch

**References**:**[isabelle] Extra type variables in constdef***From:*Nicole Rauch

- Previous by Date: [isabelle] Extra type variables in constdef
- Next by Date: Re: [isabelle] Extra type variables in constdef
- Previous by Thread: [isabelle] Extra type variables in constdef
- Next by Thread: Re: [isabelle] Extra type variables in constdef
- Cl-isabelle-users September 2007 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