Zulip Chat Archive

Stream: new members

Topic: Differences between (...), {...} and [...]

view this post on Zulip Valentin Vinoles (Apr 13 2020 at 20:08):


I have troubles to understand what is the differences between using (...), {...} and [...]. For instance, the three following possibilities seem to work, but are they the same ? If not, what are the differences and what should I use ?

variable (i : nat)
variable {j : nat}
variable [k : nat]

For instance, in some tutorials, I saw lines like

variables {X : Type} [G : group X] (x : X) (y : X)

that suggest that they must be differences (if not why using three different notations)...

Thanks for your help!

view this post on Zulip Kenny Lau (Apr 13 2020 at 20:09):

() is explicit argument, and [] and {} are for implicit arguments

view this post on Zulip Johan Commelin (Apr 13 2020 at 20:13):

Yup, they are quite different.
If you define

def foo (i : nat) {j : nat} [k : nat] : true := sorry

then @foo will ask you to provide 3 arguments explicitly. But if you simply use foo, then it only expects you to fill in the i argument. Lean will try to figure out the j argument using "unification". In practice, this means that it will try to figure out j from arguments that follow it.

In your example, you can see how this works. {X : Type} can be figured out from the explicit (x : X). This means that you don't have to pass the X argument explicitly to every group lemma that you use!

Finally, the k argument to foo will be figured out by "type class search". This is usually meant to be used for extra "structure" on a type, such as a group structure, or a metric space, or something like that. (In particular, [k : nat] will not really work.)

view this post on Zulip Johan Commelin (Apr 13 2020 at 20:15):

If it's still confusing, just use (), until you find that it becomes boring to pass all arguments by hand. Then you can start using the other types... and experiment with those.

view this post on Zulip Valentin Vinoles (Apr 14 2020 at 10:03):

Ok thanks you so much !

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 10:36):

PS did you really see [G : group X] and not just [group X]?

view this post on Zulip orlando (Apr 14 2020 at 11:38):

@Kevin Buzzard : if i understand [G : group X ] is the same as [group X] except we have named by G the hypothesis ' XX is a group ' , is it ok ?

view this post on Zulip Scott Morrison (Apr 14 2020 at 12:33):

(But usually one would only give a name G to the typeclass if you're doing something complicated, or doing something wrong! The whole design of typeclass intends that you never have to refer to them directly.)

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 13:27):

The idea is that there should only be one construction of a group structure on X, so why bother giving it a name? You can get it with by apply_instance if you need it, and you probably don't need it because the type class system will deal with it for you

Last updated: May 08 2021 at 19:11 UTC