Commit 2021-08-26 11:17 3287c942

refactor(tactic/ext): simplify ext attribute (#8785) This simplifies the ext attribute from taking a list with *, (->) and names to just @[ext] or @[ext ident]. The (->) option is only used once, in the file that declares the ext attribute itself, so it's not worth the parser complexity. The ability to remove attributes with @[ext -foo] is removed, but I don't think it was tested because it was never used and doesn't work anyway. Also fixes an issue with ext attributes being quadratic (in the number of ext attributes applied), and also makes ext attributes remove themselves (the real work of ext attributes is done by two internal attributes _ext_core and _ext_lemma_core), so that they don't pollute #print output. Before:

#print funext
@[_ext_lemma_core, ext list.cons.{0} ext_param_type (sum.inr.{0 0} (option.{0} name) (option.{0} name) (option.some.{0} name (name.mk_numeral (unsigned.of_nat' (has_zero.zero.{0} nat nat.has_zero)) name.anonymous))) (list.cons.{0} ext_param_type (sum.inr.{0 0} (option.{0} name) (option.{0} name) (option.some.{0} name (name.mk_string "thunk" name.anonymous))) (list.nil.{0} ext_param_type)), intro!]
theorem funext : ∀ {α : Sort u} {β : α → Sort v} {f₁ f₂ : Π (x : α), β x}, (∀ (x : α), f₁ x = f₂ x) → f₁ = f₂ :=

After:

#print funext
@[_ext_lemma_core, intro!]
theorem funext : ∀ {α : Sort u} {β : α → Sort v} {f₁ f₂ : Π (x : α), β x}, (∀ (x : α), f₁ x = f₂ x) → f₁ = f₂ :=