side — Mathlib

Lean4
meta def side : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "mono.side" `Mathlib.Tactic.Monotonicity.mono.side
    (ParserDescr.binary✝ `orelse
      (ParserDescr.nodeWithAntiquot✝ "left" `token.left
        ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "left" false✝))
      (ParserDescr.binary✝ `orelse
        (ParserDescr.nodeWithAntiquot✝ "right" `token.right
          ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "right" false✝))
        (ParserDescr.nodeWithAntiquot✝ "both" `token.both
          ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "both" false✝))))
Похожие утверждения