Re: [isabelle] A Newbie question about forward-proofs.

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



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.