Single braces{⋯}
indicate a maximally inserted implicit argument and {{⋯}}
a weakly inserted implicit argument, as explained in the manual.
Consider the definition of the identity map in which the first argument is implicit:
def id {α : Type u} (x : α) : α := x
In an expression such as id 3
Lean will figure out the implicit argument α
to be ℕ
. But what will it do when faced just with id
, not applied to anything? There are two options:
It could create a new meta-variable ?M
(also known as an existential variable) and convert the lone id
to id ?M
. The value of ?M
will be determined later as more information becomes available. This is known as a maximally inserted implicit argument, because it is inserted whenever possible. The above definition does so.
Indicate that the argument should not be maximally inserted by using {{⋯}}
instead:
def id {{α : Type u}} (x : α) : α := x
Now, when faced with id
, Lean will read it precisely as id
without inserting anything. This strategy is known as weakly inserted implicit arguments.
Let's try it out:
universe u
def id₁ {α : Type u} (x : α) : α := x
#check id₁
-- output: id₁ : ?M_1 → ?M_1
def id₂ {{α : Type u}} (x : α) : α := x
#check id₂
-- output: id₂ : Π ⦃α : Type u_1⦄, α → α
In most cases the difference between the maximally and weakly inserted arguments does not matter. But when it does matter it becomes very annoying if only the wrong one is available. For example, the OP shows the definition of injective map using {{⋯}}
. They are there, because with {⋯}
the expression injective f
would mean injective f ?a₁ ?a₂
which reads “for some fixed but yet to be determined a₁
and a₂
, if f a₁ = f a₂
then a₁ = a₂
". That's not what “f
is injective“ means.