# Zulip Chat Archive

## Stream: lean4

### Topic: OfNat

#### François G. Dorais (Mar 02 2021 at 18:31):

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 (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 `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 (Mar 02 2021 at 18:57):

I see, with this `natLit!`

version, `#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