alias is noncomputable

Stream: mathlib4

[Mario Carneiro]

MWE?

[Eric Wieser]

import Mathlib.Tactic.Alias

def foo : ℕ → ℕ := id

alias foo ← bar

-- failed to compile definition, consider marking it as 'noncomputable' because it depends on 'bar', and it does not have executable code
def baz (n : ℕ) := bar n

[Notification Bot]

2 messages were moved here from #mathlib4 > !4#3169 by Eric Wieser.

[Alex J. Best]

I made !4#3719 for this