Lean4
/-- A simp set for the `pnat_to_nat` tactic. -/
@[attr_parser 1000]
public meta def pnat_to_nat_coe : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Parser.Attr.pnat_to_nat_coe 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "pnat_to_nat_coe" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `orelse Lean.Parser.Tactic.simpPre Lean.Parser.Tactic.simpPost)))
(ParserDescr.unary✝ `optional
(ParserDescr.unary✝ `patternIgnore
(ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "← " `token.«← » (ParserDescr.symbol✝ "← "))
(ParserDescr.nodeWithAntiquot✝ "<- " `token.«<- » (ParserDescr.symbol✝ "<- "))))))
(ParserDescr.unary✝ `optional (ParserDescr.cat✝ `prio 0)))
