alias does not open namespace

Stream: general

[Yaël Dillies]

alias is inconsistent with def/theorem about whether the namespaces of the declarations should be automatically opened:

import Std.Tactic.Alias

def Foo.bar : Nat := 0

alias Foo.baz := bar -- unknown constant 'bar'

def Foo.baz := bar -- works

[Damiano Testa]

Nifty find!

[Yaël Dillies]

@Mario Carneiro, should I open an issue to Std?

[Yaël Dillies]

batteries#810