## Stream: new members

### Topic: snytax question about {} and []

#### Jeremy Teitelbaum (Jan 12 2022 at 17:03):

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 (Jan 12 2022 at 17:06):

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 (Jan 12 2022 at 17:08):

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 (Jan 12 2022 at 17:09):

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

#### Jeremy Teitelbaum (Jan 12 2022 at 17:10):

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

#### Eric Rodriguez (Jan 12 2022 at 17:13):

this syntax has always comfused me

#### Jeremy Teitelbaum (Jan 12 2022 at 17:14):

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

#### Reid Barton (Jan 12 2022 at 18:43):

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

Last updated: Dec 20 2023 at 11:08 UTC