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

Stream: new members

[Valentin Vinoles]

Hello,

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!

[Kenny Lau]

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

[Johan Commelin]

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.)

[Johan Commelin]

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.

[Valentin Vinoles]

Ok thanks you so much !

[Kevin Buzzard]

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

[orlando]

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

[Scott Morrison]

(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.)

[Kevin Buzzard]

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