*To*: Joe Fredette <jfredett at gmail.com>*Subject*: Re: [isabelle] A Newbie question about forward-proofs.*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Fri, 30 Oct 2009 08:28:09 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <D652183C-2CF9-405E-815F-215D27FD0579@gmail.com>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <EA6D7A3F-52CD-48DB-9508-6489EF4F802E@gmail.com> <4AE9644E.9080106@informatik.tu-muenchen.de> <D652183C-2CF9-405E-815F-215D27FD0579@gmail.com>*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

Hi Joe, > If I can bother you with another question. I wanted to get `ivr` to have > a prefix unary syntax (or a postfix, the problem (I imagine) is > isomorphic), once again, I just can't seem to find a suitable > incantation. The big tutorial (the 200+ page one) talks about using > datatypes somewhere for this purpose, But I don't see how that helps me > here. You can attach syntax to constants using "notation", e.g. notation ivr ("INV _") C.f. the Isabelle Reference Manual, keyword "notation". > Further, another (semi-related) question. In Haskell (which is where my > background lies), one can do associated datatypes, eg > > class Foo a where > data Bar a :: * -> * > bar :: Bar a b -> b -> (a,b) > --whatever > > is there an analog in Isabelle? Isabelle's type classes are, compared to Haskell, very simplistic: operations of type classes are polymorphic in *exactly* one variable; all those fancy Haskell extensions (multiple parameters, polymorphism, constructor classes, associated types) are not present. Hope this helps Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] A Newbie question about forward-proofs.***From:*Joe Fredette

**Re: [isabelle] A Newbie question about forward-proofs.***From:*Florian Haftmann

**Re: [isabelle] A Newbie question about forward-proofs.***From:*Joe Fredette

- Previous by Date: Re: [isabelle] A Newbie question about forward-proofs.
- Next by Date: [isabelle] New AFP article: The Worker/Wrapper Transformation
- Previous by Thread: Re: [isabelle] A Newbie question about forward-proofs.
- Next by Thread: [isabelle] New AFP article: The Worker/Wrapper Transformation
- Cl-isabelle-users October 2009 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