OfNat

Stream: lean4

[François G. Dorais]

How does OfNat work?

inductive Bit | bit0 | bit1

instance : OfNat Bit 0 where ofNat := Bit.bit0
instance : OfNat Bit 1 where ofNat := Bit.bit1

#synth OfNat Bit 1 -- works: instOfNatBit_1

def test : Bit := 1 -- fails!?

Setting option trace.Meta.synthInstance shows that test doesn't find instOfNatBit_1 and only finds hasOfNatOfCoe, but the #synth finds both.

[Daniel Selsam]

The instance discrimination tree is not considering it in the def test case. Currently, you need instance : OfNat Bit (noindex! 1) where ofNat := Bit.bit1 It is a known annoyance/gotcha and may be addressed.

[François G. Dorais]

Makes sense. I need to get used to these discrimination trees... Thanks!

[Leonardo de Moura]

@François G. Dorais The section Numerals at https://leanprover.github.io/lean4/doc/typeclass.html explains how OfNat works. The OfNat instances must be indexed with "raw numerals". A "raw numeral" is a numeral that is not wrapped with OfNat.ofNat.
You can create raw numerals using the notation natLit! n. Here is your example with this notation.

inductive Bit | bit0 | bit1

instance : OfNat Bit (natLit! 0) where ofNat := Bit.bit0
instance : OfNat Bit (natLit! 1) where ofNat := Bit.bit1

def test1 : Bit := 1 -- works
def test0 : Bit := 0 -- works

The indexing will work as expected in the example above.
The noindex! trick that @Daniel Selsam suggested works too, but if you have instances for different numerals, it will impact performance because Lean will not be able to filter them out using the discrimination trees.

[François G. Dorais]

I see, with this natLit! version, #synth OfNat Bit 1 fails because the 1 is actually ofNat Nat (natLit! 1). Very interesting!