Zulip Chat Archive

Stream: new members

Topic: What does @@ mean?

Daniel Fabian (Jun 01 2020 at 13:05):

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 (Jun 01 2020 at 13:13):

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 (Jun 01 2020 at 13:16):

ah, great. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC