snytax question about {} and []

Stream: new members

[Jeremy Teitelbaum]

The definition of eq looks like this:

inductive eq {α : Sort u} (a : α) : α → Prop
| refl [] : eq a

What is the significance of the []? I guess it has something to do with an implicit argument "that can be inferred by typeclass inference" but I don't know what it might be referring to specifically.

Similarly, the definition of 'list' *in the reference manual, though not in core.init, looks like this:

inductive list (α : Type u)
| nil {} : list
| cons (a : α) (l : list) : list

Again I guess that {} is a reference to an implicit argument so that you can say which particular kind of empty list you have (i.e. an empty list of natural numbers, for example.) But why isn't it used in the mathlib code?

[Kyle Miller]

I don't remember where this is documented, but what these do is alter whether the arguments to eq or list themselves are implicit or not for the constructor.

[Kyle Miller]

Compare:

namespace test1

inductive eq {α : Sort u} (a : α) : α → Prop
| refl [] : eq a

#print eq
/-
inductive test1.eq : Π {α : Sort u}, α → α → Prop
constructors:
test1.eq.refl : ∀ {α : Sort u} (a : α), eq a a
-/

end test1

namespace test2

inductive eq {α : Sort u} (a : α) : α → Prop
| refl : eq a

#print eq
/-
inductive test2.eq : Π {α : Sort u}, α → α → Prop
constructors:
test2.eq.refl : ∀ {α : Sort u} {a : α}, eq a a
-/

end test2

[Kyle Miller]

It doesn't seem that {} in the definition of list does anything anymore.

[Jeremy Teitelbaum]

It's weird that the syntax for eq is [] rather than {}, given the behavior you illustrate.

[Eric Rodriguez]

this syntax has always comfused me

[Alex J. Best]

Some previous discussion at https://leanprover-community.github.io/archive/stream/236446-Type-theory/topic/The.20.60.7B.7D.60.20annotation.20for.20inductive.20types.html, see lean#175 too

[Jeremy Teitelbaum]

I take it back, it's weirder than I thought. The [] makes the argument explicit; the default is implicit.

[Reid Barton]

This syntax changed in the community version of Lean so it may not be (accurately) documented anywhere.