What does @@ mean?

Stream: new members

[Daniel Fabian]

I understand that without an @ annotation, implicit arguments are inferred, with a @ annotation, all the arguments are unfolded. But what happens with @@?

Here's a snippet of what I'm working on:

import data.set
variables {α : Type*} {β : Type*} {ι : Type*}
variable {π : ι → Type*}
/--
  We define a cartesian product by a point-wise equivalence between α and its projections π.
 -/
structure cartesian_product (α : Type*) (π : ι → Type*) :=
(mapping : α ≃ Π i, π i)

def cartesian_product.proj (P : cartesian_product α π) (A : set α) (i : ι) : set (π i) :=
(λ a, P.mapping a i) '' A

def cartesian_product.prod (P : cartesian_product α π) (Bᵢ : Π i, set (π i)) : set α :=
P.mapping.symm '' { b | ∀ i, b i ∈ Bᵢ i }

variable { P : cartesian_product α π }

@[simp]def subspace (A : set α) :=
A = (P.prod ∘ P.proj) A

#check subspace
#check @subspace
#check @@subspace

and the output is:

subspace : set ?M_1 → Prop
@subspace : Π {α : Type u_5} {ι : Type u_6} {π : ι → Type u_7} {P : cartesian_product α π}, set α → Prop
@@subspace : Π {π : ?M_2 → Type u_7} {P : cartesian_product ?M_1 π}, set ?M_1 → Prop

[Reid Barton]

I think it means: automatically fill all implicit arguments up to (and not including) the first one which depends on an earlier argument.

[Daniel Fabian]

ah, great. Thanks!