Lean4
/-- The simpset `qify_simps` is used by the tactic `qify` to move expressions from `ℕ` or `ℤ` to `ℚ`
which gives a well-behaved division. -/
@[attr_parser 1000]
public meta def qify_simps : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Parser.Attr.qify_simps 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "qify_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)))
