to_additive and noncomputable

Stream: mathlib4

[Yakov Pechersky]

The plain @[to_additive] decorator does not properly transmit noncomputable to the derived definition. It works fine if the tagging is done after the fact:

import Mathlib.Tactic.ToAdditive

@[to_additive Bar]
def Foo (a : α) : α := a

@[to_additive Bar.bar] -- this does not work
noncomputable def Foo.foo (h : ∃ _ : α, True) : α := Classical.choose h

noncomputable def Foo.foo2 (h : ∃ _ : α, True) : α := Classical.choose h
noncomputable def Bar.baz (h : ∃ _ : α, True) : α := Classical.choose h

attribute [to_additive Bar.baz] Foo.foo2 -- this works

[Alex J. Best]

mathlib4#625