In Lean, what do double curly brackets mean?

Question

In Lean, explicit function arguments are enclosed in round brackets and implicit ones in curly brackets, as in this example:

lemma surjective.comp {g : β → φ} {f : α → β} (hg : surjective g) (hf : surjective f) :
  surjective (g ∘ f) := ...

However, occasionally we see some strange double curly brackets like this:

def injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂

I'm sure I once read an explanation of this, but my attempts to search for it now have failed. What do the double curly brackets mean?

Answer 1

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:

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

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