How does @ work?

Stream: new members

[Anh Luong]

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]

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]

See also the end of Section 2.9 in TPiL.

[Anh Luong]

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

[Eric Wieser]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I think I prefer the lean 4 solution :-)

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

You can find more information on attributes here