tfaeHave' — Mathlib

Lean4
@[inherit_doc tfaeHave, tactic_parser 1000]
public meta def tfaeHave' : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.TFAE.tfaeHave' 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "tfae_have " false✝)
      (ParserDescr.parser✝
        (Lean.Name.mkStr✝
          (Lean.Name.mkStr✝
            (Lean.Name.mkStr✝
              (Lean.Name.mkStr✝
                (Lean.Name.mkStr✝
                  (Lean.Name.mkNum✝
                    (Lean.Name.mkStr✝
                      (Lean.Name.mkStr✝ (Lean.Name.mkStr✝ (Lean.Name.mkStr✝ Lean.Name.anonymous✝ "_private") "Mathlib")
                        "Tactic")
                      "TFAE")
                    0)
                  "Mathlib")
                "Tactic")
              "TFAE")
            "Parser")
          "tfaeHaveIdLhs")))
Похожие утверждения