Zulip Chat Archive

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?

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

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: Dec 20 2023 at 11:08 UTC