Lean4
/-- 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](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20Polynomial.2Ecoeff.20example/near/395438147).
-/
@[term_parser 1000]
public meta def «termOfNat(_)» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `«termOfNat(_)» 1024
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "ofNat(") (ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ ")"))
