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

Stream: new members

[Eric Wieser]

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]

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]

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

[Mario Carneiro]

{} means all parameters are implicit

[Eric Wieser]

As in, the projections have that implitness?

[Mario Carneiro]

yes

[Mario Carneiro]

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]

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

[Mario Carneiro]

it's not that expressive

[Eric Wieser]

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

[Mario Carneiro]

you just get the three mentioned settings (and none)

[Eric Wieser]

So () is legal too?

[Mario Carneiro]

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

[Mario Carneiro]

actually it is ( ) because of parser issues

[Mario Carneiro]

docs#environment.implicit_infer_kind

[Eric Wieser]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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