Lean4
/-- A simp set for the `fin_omega` wrapper around `omega`. -/
@[attr_parser 1000]
public meta def fin_omega : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Parser.Attr.fin_omega 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "fin_omega" 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)))
