variable

Stream: lean4

[Yury G. Kudryashov]

The following doesn't work:

variable (α : Type _) [Nonempty α]

def h [Nonempty α] := α

variable {α} (x : h α)

while the following works:

variable (α : Type _) [Nonempty α]

def h [Nonempty α] := α

variable {α}
variable (x : h α)

[Jakob von Raumer]

Noticed this as well when porting. The issue seems to be that variable seems to either change visibility of existing variables OR introduce new one but not both?

[Eric Wieser]

If the behavior of performing one action or the other but not both is deliberate, should the two actions have different spellings? (eg variable vs variable update)

[Kevin Buzzard]

This discussion should be moved to #lean4

[Notification Bot]

This topic was moved here from #mathlib4 > variable by Eric Wieser.

[Yury G. Kudryashov]

It complains that it can't find [Nonempty α], so probably the issue is that (x : h α) is evaluated in a context that does not include previously defined (in a variable) instances.