366.lean:1:0-2:72: warning: Definition `foo` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
[Meta.synthInstance] ✅️ Inhabited Nat
  [Meta.synthInstance] ✅️ new goal Inhabited Nat
    [Meta.synthInstance.instances] #[@instInhabitedOfMonad, instInhabitedNat]
  [Meta.synthInstance.apply] ✅️ apply instInhabitedNat to Inhabited Nat
    [Meta.synthInstance.tryResolve] ✅️ Inhabited Nat ≟ Inhabited Nat
    [Meta.synthInstance.answer] ✅️ Inhabited Nat
  [Meta.synthInstance] result instInhabitedNat