| 297.lean:1:10-1:11: error: failed to synthesize | |
| OfNat (Sort ?u) 0 | |
| numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is | |
| Sort ?u | |
| due to the absence of the instance above | |
| use `set_option diagnostics true` to get diagnostic information |