Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 14 2020 at 20:41):

{} means all parameters are implicit

view this post on Zulip Eric Wieser (Nov 14 2020 at 20:42):

As in, the projections have that implitness?

view this post on Zulip Mario Carneiro (Nov 14 2020 at 20:42):

yes

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 14 2020 at 20:43):

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

view this post on Zulip Mario Carneiro (Nov 14 2020 at 20:43):

it's not that expressive

view this post on Zulip Eric Wieser (Nov 14 2020 at 20:43):

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

view this post on Zulip Mario Carneiro (Nov 14 2020 at 20:43):

you just get the three mentioned settings (and none)

view this post on Zulip Eric Wieser (Nov 14 2020 at 20:43):

So () is legal too?

view this post on Zulip Mario Carneiro (Nov 14 2020 at 20:44):

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

view this post on Zulip Mario Carneiro (Nov 14 2020 at 20:44):

actually it is ( ) because of parser issues

view this post on Zulip Mario Carneiro (Nov 14 2020 at 20:46):

docs#environment.implicit_infer_kind

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 14 2020 at 20:47):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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