Remove attribute?

Stream: general

[Mathieu Guay-Paquet]

I have a structure that I'm tagging with @[ext] to generate an ext lemma, but then I want to define a better ext lemma for the structure, using the tactic-generated one. Is there a way to then remove the ext attribute from the tactic-generated lemma?

[Alex J. Best]

Do you need to remove it? I just did some silly experiments and it seems the most recently tagged one takes priority? Does that work in your setting?

import tactic
example : (λ n, n) = λ n, n + 1 :=
begin
ext,
end
@[ext]
lemma my_amazing_ext (f g : ℕ → ℕ) (h : f 1 = g 1): f = g := sorry
example : (λ n, n) = λ n, n + 1 :=
begin
ext,
end
@[ext]
lemma my_amazing_ext' (f g : ℕ → ℕ) (h : f 2 = g 2): f = g := sorry
example : (λ n, n) = λ n, n + 1 :=
begin
ext,
end
@[ext]
lemma my_amazing_ext'' (f g : ℕ → ℕ) (h : f 1 = g 1): f = g := sorry
example : (λ n, n) = λ n, n + 1 :=
begin
ext,
end

[Mario Carneiro]

You can remove attributes with attribute [-ext] lem but there are some constraints on its use

[Alex J. Best]

removing ext gives an error message

[Mario Carneiro]

That said, it does give an error message to use local attributes and that does have the desired effect

[Mario Carneiro]

import tactic
example : (λ n, n) = λ n, n + 1 :=
by ext -- x = x + 1

section
local attribute [ext]
lemma my_amazing_ext (f g : ℕ → ℕ) (h : f 1 = g 1): f = g := sorry

example : (λ n, n) = λ n, n + 1 :=
by ext -- 1 = 1 + 1

end

example : (λ n, n) = λ n, n + 1 :=
by ext -- x = x + 1

[Alex J. Best]

But if you tag a structure with @[ext] it won't be a local attribute right?

[Mario Carneiro]

This works as long as the scope of the first local ext lemma is fairly localized, to say the first half of a file, although you can make it last longer using locales if necessary

[Mario Carneiro]

seems to work:

import tactic

section
local attribute [ext]
structure test := (x : ℕ)

example (f g : test) : f = g :=
by ext -- f.x = g.x

end

example (f g : test) : f = g :=
by ext -- no ext rule found

[Mathieu Guay-Paquet]

Ah, great! Thanks to both of you, I think this is giving me all the tools I need