## Stream: new members

### Topic: What do empty () [] {} mean in struct fields?

#### Eric Wieser (Nov 14 2020 at 20:38):

I found this notation in mathlib just now:

class is_semiring_hom {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α → β) : Prop :=
(map_zero [] : f 0 = 0)
(map_one [] : f 1 = 1)


I think I've also seen {} used in inductive types, and am now extrapolating that () is also legal. What does the [] mean?

#### Kevin Buzzard (Nov 14 2020 at 20:40):

This is a deprecated class, right? But I don't know the answer. You can find out yourself with #check @is_semiring_hom.map_zero right?

#### Mario Carneiro (Nov 14 2020 at 20:40):

it means the opposite of {} more or less: parameters get the same implicitness as the way they are declared in the class

#### Mario Carneiro (Nov 14 2020 at 20:41):

{} means all parameters are implicit

#### Eric Wieser (Nov 14 2020 at 20:42):

As in, the projections have that implitness?

yes

#### Mario Carneiro (Nov 14 2020 at 20:42):

the stated implicitness is usually only for the class itself, so this notation lets you change the implicitness of the arguments that lean supplies to the fields

#### Eric Wieser (Nov 14 2020 at 20:43):

can you use it to change the explicitness of just some arguments?

#### Mario Carneiro (Nov 14 2020 at 20:43):

it's not that expressive

#### Eric Wieser (Nov 14 2020 at 20:43):

(or alternatively - is there any documentation / reference on the extent of this syntax?)

#### Mario Carneiro (Nov 14 2020 at 20:43):

you just get the three mentioned settings (and none)

#### Eric Wieser (Nov 14 2020 at 20:43):

So () is legal too?

#### Mario Carneiro (Nov 14 2020 at 20:44):

yes, it means everything is explicit - I've never seen that being useful

#### Mario Carneiro (Nov 14 2020 at 20:44):

actually it is ( ) because of parser issues

#### Mario Carneiro (Nov 14 2020 at 20:46):

docs#environment.implicit_infer_kind

#### Eric Wieser (Nov 14 2020 at 20:46):

structure unusual (A : Type*) {B : Type*} [C : Type*] :=
(square [] : unit)
(round ( ) : unit)
(curly {} : unit)

#check @unusual.square
-- unusual.square : Π {A : Type u_1} {B : Type u_2} [C : Type u_3], unusual A → unit
#check @unusual.round
-- unusual.round : Π (A : Type u_1) (B : Type u_2) [C : Type u_3], unusual A → unit
#check @unusual.curly
-- unusual.curly : Π {A : Type u_1} {B : Type u_2} [C : Type u_3], unusual A → unit


#### Eric Wieser (Nov 14 2020 at 20:47):

I don't see the difference between{} and []

#### Mario Carneiro (Nov 14 2020 at 20:50):

inductive unusual (A : Type) {B : Type} [C : Type] : Type
| square [] : unusual
| round ( ) : unusual
| curly {} : unusual
#print unusual

-- inductive unusual : Type → Π {B : Type} [C : Type], Type
-- constructors:
-- unusual.square : Π (A : Type) {B : Type} [C : Type], unusual A
-- unusual.round : Π (A : Type) {B : Type} [C : Type], unusual A
-- unusual.curly : Π {A B : Type} [C : Type], unusual A


#### Mario Carneiro (Nov 14 2020 at 20:52):

With [], a parameter is only made implicit if there is a later dependent hypothesis (i.e. our usual conventions)

#### Mario Carneiro (Nov 14 2020 at 20:52):

You can't see the difference with a structure because the unusual A argument is always going to depend on all the parameters

Last updated: May 14 2021 at 21:11 UTC