François G. Dorais (Mar 02 2021 at 18:31):
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!?
trace.Meta.synthInstance shows that
test doesn't find
instOfNatBit_1 and only finds
hasOfNatOfCoe, but the
#synth finds both.
Daniel Selsam (Mar 02 2021 at 18:40):
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 (Mar 02 2021 at 18:46):
Makes sense. I need to get used to these discrimination trees... Thanks!
Leonardo de Moura (Mar 02 2021 at 18:48):
@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
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.
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 (Mar 02 2021 at 18:57):
I see, with this
#synth OfNat Bit 1 fails because the
1 is actually
ofNat Nat (natLit! 1). Very interesting!
Last updated: May 18 2021 at 22:15 UTC