<div class="gmail_quote">On Mon, Apr 20, 2009 at 8:44 AM, Tillmann Rendel <span dir="ltr"><<a href="mailto:rendel@cs.au.dk">rendel@cs.au.dk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
However, I would prefer the following Coq-like syntax:<br>
<br>
data Maybe a =<br>
| Just a<br>
| Nothing</blockquote><div><br></div><div>Of course, Coq's inductive syntax is just GADT form:</div><div><br></div><div>Inductive Maybe a :=</div><div>| Just : a -> Maybe a</div><div>| Nothing : Maybe a.</div>
<div><br></div><div>data Maybe a where</div><div> Just :: a -> Maybe a</div><div> Nothing :: Maybe a</div><div><br></div><div>I find GADT syntax much clearer than H98 syntax, so I use it when I'm not being picky about compatibility. :-)</div>
<div><br></div><div>(And yes, I know you just meant the optional leading bar)</div><div><br></div><div>Luke</div></div>