Zulip Chat Archive

Stream: new members

Topic: What does @@ mean?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Daniel Fabian (Jun 01 2020 at 13:16):

ah, great. Thanks!

Last updated: May 10 2021 at 23:11 UTC