The ofNat() macro

def «termOfNat(_)» : Lean.ParserDescr

This macro is a shorthand for OfNat.ofNat combined with no_index.

When writing lemmas about OfNat.ofNat, the term needs to be wrapped in no_index so as not to confuse simp, as no_index (OfNat.ofNat n).

Some discussion is on Zulip here.

Equations

• One or more equations did not get rendered due to their size.