syntax of inductive definitions

Stream: general

[Bernd Losert]

I'm reading https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html and it says:

The first character | in an inductive declaration is optional. We can also separate constructors using a comma instead of |.

However, if I remove the first | I get an error. And if I use commas I also get an error. Could it be that this syntax is no longer supported?

Also, how do you define GADTs in Lean? The end type of each constructor is always the name of the type, so there doesn't seem to be a way to define constructors for a GADT.

I'm using Lean 3 by the way.

[Mario Carneiro]

inductive my_gadt : nat -> Type
| foo : my_gadt 0
| bar (n) : my_gadt n -> my_gadt (2 * n + 1)

[Mario Carneiro]

the first | in an inductive definition is not optional

[Mario Carneiro]

and you can't use commas

[Mario Carneiro]

that sounds like out of date info

[Bernd Losert]

Cool. Thanks.

[Mario Carneiro]

leanprover/theorem_proving_in_lean#115

[Bernd Losert]

That's a 404 page.

[Adam Topaz]

It's the linkifier issue. I guess Mario means
https://github.com/leanprover/theorem_proving_in_lean/pull/115 ?

[Mario Carneiro]

that's weird, github normally redirects /issues/N pages to /pull/N

[Adam Topaz]

https://leanprover.zulipchat.com/#narrow/stream/236604-Zulip-meta/topic/linkifier.20to.20PRs/near/264364086