Zulip Chat Archive

Stream: general

Topic: local notation and implicit variables

Andrew Yang (Jan 22 2022 at 13:41):

In the following code, the argument α is explicit in foo despite the variable {α} before it. Is this intended? Could I somehow make it implicit?

variable (α : Type)

local notation `β` := α

variable {α}

def foo : β  β := id

#check foo -- gives `foo : Π (α : Type), α → α`

Eric Wieser (Jan 22 2022 at 15:41):

This has come up before, but I don't remember having as short a mwe last time, so thanks for that

Last updated: Aug 03 2023 at 10:10 UTC