empty {} in inductive type definition

Stream: new members

[Juan Pablo Romero]

Hi, I'm trying to understand why the empty brackets are useful in definitions like this:

inductive list (α : Type*)
| nil {} : list
| cons : α → list → list

With or without it Leans reports the type of @list.nil as : Π {α : Type}, list α.

[Mario Carneiro]

It's vestigial; the default was changed to {}, and the old default is now accessible with []

[Kevin Buzzard]

That is correct -- they're not useful. Older literature might have them -- there was a refactor.