Zulip Chat Archive

Stream: lean4

Topic: OfNat abbreviation


view this post on Zulip Kyle Miller (Jan 09 2021 at 05:21):

I can see this not being supported, but I wanted to check whether this HasOne abbreviation should work:

/- ok: -/
def one (α : Type u) [OfNat α (natLit! 1)] : α := 1

abbrev HasOne (α : Type u) := OfNat α (natLit! 1)

/- Not ok: "failed to synthesize instance" -/
def one' (α : Type u) [HasOne α] : α := 1

/- ok: -/
example : HasOne Nat := inferInstance

view this post on Zulip Leonardo de Moura (Jan 12 2021 at 15:00):

Pushed fix https://github.com/leanprover/lean4/commit/b5fdc5e3641130b42d0307fe814ffdf32aa25583


Last updated: May 18 2021 at 22:15 UTC