On Mon, Apr 20, 2009 at 8:44 AM, Tillmann Rendel <rendel@cs.au.dk> wrote:

However, I would prefer the following Coq-like syntax:

data Maybe a =
| Just a
| Nothing

Of course, Coq's inductive syntax is just GADT form:

Inductive Maybe a :=

| Just : a -> Maybe a

| Nothing : Maybe a.

data Maybe a where

Just :: a -> Maybe a

Nothing :: Maybe a

I find GADT syntax much clearer than H98 syntax, so I use it when I'm not being picky about compatibility. :-)

(And yes, I know you just meant the optional leading bar)

Luke