OfNat abbreviation

Stream: lean4

[Kyle Miller]

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

[Leonardo de Moura]

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