## Stream: lean4

### Topic: unfortunate error messages

#### Jason Gross (Mar 11 2021 at 20:39):

This is unfortunate:

instance OfNat_1 : OfNat Type 1 := { ofNat := Unit }
#check (1 : Type)
/-
2:9: failed to synthesize instance
OfNat Type 1
-/


#### Jason Gross (Mar 11 2021 at 20:39):

(I do see what's going on here, but it took me a couple minutes and set_option pp.all true to puzzle it out)

#### Leonardo de Moura (Mar 11 2021 at 20:43):

We have some documentation here https://leanprover.github.io/lean4/doc/typeclass.html (Numerals section)
You are not the first person confused by this issue, we should probably just let people write these instances without the natLit!.

Last updated: May 07 2021 at 12:15 UTC