Basic question about inductive types

Stream: general

[Morgan Sinclaire]

I’m reading TPIL and Ch. 7 on inductive types has this simple example:

inductive Weekday where
  | friday

It also says that “The first character | in an inductive declaration is optional. We can also separate constructors using a comma instead of |.” But when I try these examples:

inductive Weekday' where
    friday

inductive Weekday'' where
  , friday

they fail to compile (regardless of the indentation I've tried). Am I misunderstanding that TPIL quote?

[Daniel Weber]

I'd guess that this is a leftover from Lean 3 and is false for Lean 4

[Kim Morrison]

@Morgan S, if you'd like to open an issue, you can click the github icon in the top right of the TPIL page. It would be very helpful!

[Morgan Sinclaire]

Just submitted, thanks for the responses!