*To*: Steve W <s.wong.731 at gmail.com>*Subject*: Re: [isabelle] Type as argument*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Fri, 13 May 2011 21:26:22 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BANLkTinYY-raTBNuUT6i-t9pX48g7BU9nQ@mail.gmail.com>*References*: <BANLkTin0NNwByvPfmmnMZGMo0Wm0yrXCBw@mail.gmail.com> <BANLkTinT-2mQ7--5Y9ADLDCOrt9uW_dbVw@mail.gmail.com> <BANLkTinYY-raTBNuUT6i-t9pX48g7BU9nQ@mail.gmail.com>

> 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

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

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

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

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

- Previous by Date: Re: [isabelle] Type as argument
- Next by Date: Re: [isabelle] Type as argument
- 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