tacticGeneralize'_:_=_ — Mathlib

Lean4

/-- Backwards compatibility shim for `generalize`. -/
@[tactic_parser 1000]
public meta def «tacticGeneralize'_:_=_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `«tacticGeneralize'_:_=_» 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "generalize'" false✝)
              (ParserDescr.const✝ `ident))
            (ParserDescr.symbol✝ " : "))
          (ParserDescr.cat✝ `term 51))
        (ParserDescr.symbol✝ " = "))
      (ParserDescr.const✝ `ident))

Похожие утверждения