*To*: Steve W <s.wong.731 at gmail.com>*Subject*: Re: [isabelle] Type as argument*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Mon, 16 May 2011 07:53:52 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, René Thiemann <rene.thiemann at uibk.ac.at>*In-reply-to*: <BANLkTimp_-pfeFwmA6ayxAe6Xn73S0OcRg@mail.gmail.com>*References*: <BANLkTin0NNwByvPfmmnMZGMo0Wm0yrXCBw@mail.gmail.com> <BANLkTinT-2mQ7--5Y9ADLDCOrt9uW_dbVw@mail.gmail.com> <BANLkTinYY-raTBNuUT6i-t9pX48g7BU9nQ@mail.gmail.com> <E17FCF41-BDC0-4FDA-8CA8-194B28B2834A@uibk.ac.at> <BANLkTimp_-pfeFwmA6ayxAe6Xn73S0OcRg@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

2011/5/16 Steve W <s.wong.731 at gmail.com>: > Thanks all. One more question: what is the "itself" keyword for in "'a > itself"? The "itself" is just a type constructor. It is like what you would get from the following datatype declaration: datatype 'a itself = Type (* one constructor with no arguments *) The syntax "TYPE('a)" is an abbreviation for "Type :: 'a itself". - Brian > > Thanks > Steve > > 2011/5/13 René Thiemann <rene.thiemann at uibk.ac.at> > >> > Thanks. If I change f to a binary function: >> > >> > class foo = >> > fixes f :: "int => 'a itself => int" >> > >> > and with the following instantiation: >> > >> > instantiation nat :: foo >> > begin >> > definition "f 0 (t::nat itself) = 0" >> > instance .. >> > end >> > >> > I get an error on "0::int". It works if 0 is replaced by a free variable >> > though. Why's that? >> >> Because "definition" cannot be used with pattern matching on left-hand >> sides. >> Usually, one can use "fun" instead. However, even with "fun" you cannot >> do pattern matching on "int" instead of "nat". >> >> However, you might write "f x (t:: nat itself) = (if x = (0 :: int) then 0 >> else ...)" >> >> René >> -- >> René Thiemann mailto:rene.thiemann at uibk.ac.at >> Computational Logic Group >> http://cl-informatik.uibk.ac.at/~thiemann/ >> Institute of Computer Science phone: +43 512 507-6434 >> University of Innsbruck >> >> >

**References**:**[isabelle] Type as argument***From:*Steve W

**Re: [isabelle] Type as argument***From:*Brian Huffman

**Re: [isabelle] Type as argument***From:*Steve W

**Re: [isabelle] Type as argument***From:*René Thiemann

**Re: [isabelle] Type as argument***From:*Steve W

- Previous by Date: Re: [isabelle] Type as argument
- Next by Date: [isabelle] CFP: SSV 2011 - Workshop on Systems Software Verification [deadline extended]
- Previous by Thread: Re: [isabelle] Type as argument
- Next by Thread: Re: [isabelle] Type as argument
- Cl-isabelle-users May 2011 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