Documentation

Lean.Util.Reprove

The reprove command #

This command reproves a list of declarations with a given tactic sequence. It is useful for testing tactics.

source
def Lean.Elab.Command.reproveDecl (declName : Name) (tacticSeq : TSyntax `Lean.Parser.Tactic.tacticSeq) :
CommandElabM Unit

Reproving a declaration with a given tactic sequence

Equations
    Instances For
      source
      def Lean.Elab.Command.reprove :
      ParserDescr

      Reproves a list of declarations with a given tactic sequence.

      reprove theorem1 theorem2 theorem3 by simp
      Equations
        Instances For
          source
          def Lean.Elab.Command.elabReprove :
          CommandElab
          Equations
            Instances For