*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Subtyping*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Thu, 25 Aug 2011 13:58:21 +1200*Cc*: isabelle-users at cl.cam.ac.uk, Christian Sternagel <c.sternagel at gmail.com>*In-reply-to*: <CAP0k5J6QPfr3Bmt2sdehaeeVoW8FFFskWN6Yo0r52ZbBpcuVwQ@mail.gmail.com>*References*: <CAP0k5J7vOgpcrUqVy5s4gAsQf1zAtr4gH-wiXjj=Ge7bBHYVfQ@mail.gmail.com> <4E546478.7030708@gmail.com> <CAP0k5J6RHg1OwtJNOrjz-fh4dL7HcY3x6AsDJnnv_qBQusUuFA@mail.gmail.com> <4E54BA54.7090600@gmail.com> <CAP0k5J7thCakgLf30UNWEuwAGzrph-rrP4k2BYAAq=a1r+tF-w@mail.gmail.com> <CAP0k5J5o=28ugkz48jVYaUR9NjGktKXscXAjOKQyVpy0ennAXA@mail.gmail.com> <4E559CC4.1080703@gmail.com> <CAP0k5J6QPfr3Bmt2sdehaeeVoW8FFFskWN6Yo0r52ZbBpcuVwQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.18) Gecko/20110617 Thunderbird/3.1.11

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On 25/08/11 13:07, John Munroe wrote: > Thanks so much. It surely has been helpful! > > One thing though: I can't define the datatype "'a + 'b" with > > datatype 'a + 'b = Inl 'a | Inr 'b > > It doesn't seem to like the '+' operator. Is using "datatype ('a,'b) > sum" the only way? (I see that it doesn't have to be 'sum' but any > arbitrary name seems to do.) I don't think you need to define it. I'm pretty sure everything I said is true of the built-in sum type. However, Christian's suggestion of how it could be defined is useful to help understand how it works. If you use the built-in sum type, you can still define is_Inl as Christian suggested (a way I have little experience with), or you can define it like this: definition is_Inl :: "'a + 'b => bool" where "is_Inl x == \<exists> a. x = Inl a" > Also, is the approach of using sum type more appropriate than > overloading for my application? Would overloading allow the same > effect to be produced, i.e. defining a function that gives True only > if the input is of a particular type? I don't have much experience with overloading, so I might let someone else answer this. But their answer might depend on what your intended application really is --- what do you want to use this for? Tim <>< -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.10 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAk5VrDcACgkQ/cBxZIxl6rmq5QCcD0zBV6lXqzOkUHQETFj+3Y/4 uPoAoMXhC6dyoX+E9R+E7ehjtcLNr09A =wgW0 -----END PGP SIGNATURE-----

**References**:**[isabelle] Subtyping***From:*John Munroe

**Re: [isabelle] Subtyping***From:*Tim (McKenzie) Makarios

**Re: [isabelle] Subtyping***From:*John Munroe

**Re: [isabelle] Subtyping***From:*John Munroe

**Re: [isabelle] Subtyping***From:*John Munroe

**Re: [isabelle] Subtyping***From:*Tim (McKenzie) Makarios

**Re: [isabelle] Subtyping***From:*John Munroe

- Previous by Date: Re: [isabelle] Subtyping
- Next by Date: [isabelle] Various ways of overloading
- Previous by Thread: Re: [isabelle] Subtyping
- Next by Thread: [isabelle] Overloading in locales
- Cl-isabelle-users August 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