Lean4
/-- Simp attribute for lemmas about `Even` -/
@[attr_parser 1000]
public meta def parity_simps : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Parser.Attr.parity_simps 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "parity_simps" 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)))
