## Stream: new members

### Topic: How does @ work?

#### Anh Luong (Apr 28 2021 at 17:26):

What does putting @ before something do?

  refine_struct {
zero := (0 : ℂ),
add := (+),
neg := has_neg.neg,
sub := has_sub.sub,
one := 1,
mul := (*),
nsmul := @nsmul_rec _ ⟨(0)⟩ ⟨(+)⟩,
npow := @npow_rec _ ⟨(1)⟩ ⟨(*)⟩,
gsmul := @gsmul_rec _ ⟨(0)⟩ ⟨(+)⟩ ⟨has_neg.neg⟩
};


When I tried messing around with it earlier it seemed to change it somehow but I don't really understand what it did still. So I'm wondering what the difference and the point of it is.

#### Eric Wieser (Apr 28 2021 at 17:34):

def foo {α : Type*} (x : α) := x

#check foo   -- foo : ?M_1 → ?M_1
#check @foo  -- foo : Π {α : Type u_1}, α → α

-- @ makes the {} arguments explicit
#check foo (1 : ℕ)   -- foo 1 : ℕ
#check @foo ℕ (1 : ℕ)   -- foo 1 : ℕ

#check @foo ℕ        -- foo : ℕ → ℕ
#check @foo (1 : ℕ)  -- #check @foo ℕ  -- foo : ℕ → ℕ


#### Bryan Gin-ge Chen (Apr 28 2021 at 17:34):

See also the end of Section 2.9 in TPiL.

#### Anh Luong (Apr 28 2021 at 17:40):

Thanks @Eric Wieser and @Bryan Gin-ge Chen! I should read through that book sometime.

#### Eric Wieser (Apr 28 2021 at 17:45):

I just learnt something new about @ - it's "reset" by (... : _):

lemma many {a b} (c : ℕ) {d e} (f : ℕ) : a + b = c ∧ d + e = f := sorry

variables {a b c d e f : ℕ}

-- argument names here match the names in many above
-- the obvious ways to call it
#check many c f
#check @many a b c d e f
-- a surprising way!
#check (@many a : _) c f


#### Eric Wieser (Apr 28 2021 at 17:46):

Puzzle: is there a way of writing @many a _ c d _ f without having to pass either underscore?

#### Mario Carneiro (Apr 29 2021 at 01:51):

example : a + b = c ∧ d + e = f :=
by { have := @many a, have := this, exact (@this c d : _) f }


#### Kevin Buzzard (Apr 29 2021 at 07:22):

I think I prefer the lean 4 solution :-)

#### Eric Wieser (Apr 29 2021 at 07:26):

Would it make sense to allow @(...) as syntax, rather than requiring @ to precede an identifier?

#### Eric Wieser (Apr 29 2021 at 07:27):

(@((@many a : _) c) d : _) f would then work

#### Eric Wieser (Apr 29 2021 at 07:30):

I mean, on the one hand you probably don't want to have to write that

#### Eric Wieser (Apr 29 2021 at 07:31):

But on the other, restricting the operator to only work on identifiers feels like allowing -x but forbidding -(sin x)

#### Mario Carneiro (Apr 29 2021 at 10:59):

Eric Wieser said:

Would it make sense to allow @(...) as syntax, rather than requiring @ to precede an identifier?

Yes, I've wanted that for years and lean 4 made it happen

#### Mario Carneiro (Apr 29 2021 at 11:01):

In fact, the lean 3 pretty printer actually gets confused when printing expressions like that one because it requires @(...) but no such syntax exists

#### Mario Carneiro (Apr 29 2021 at 11:03):

def foo : ℕ := by have := (λ {x : ℕ}, x); exact @this 0
#print foo -- def foo : ℕ := λ {x : ℕ}, x       <- wrong!
set_option pp.implicit true
#print foo -- def foo : ℕ := @(λ {x : ℕ}, x) 0  <- can't type!
#check @(λ {x : ℕ}, x) 0 -- fail


#### Alex Zhang (May 25 2021 at 06:09):

In the documentation data.finset.basic, I saw image.png
What does @[simp] mean here? In particular, what is the function of @here?

#### Horatiu Cheval (May 25 2021 at 06:18):

The @here has a different meaning than the @ previously discussed in this thread.
This usage is for tagging theorems, definitions, inductives etc. with attributes.
Here finset.val_inj is tagged with the attribute simp, making it a simplification lemma, i.e. a lemma which will now be tried by the simp tactic.

#### Horatiu Cheval (May 25 2021 at 06:21):

You can find more information on attributes here

Last updated: Dec 20 2023 at 11:08 UTC