The reprove command

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

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

Reproving a declaration with a given tactic sequence

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.reprove : ParserDescr

Reproves a list of declarations with a given tactic sequence.

reprove theorem1 theorem2 theorem3 by simp

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.elabReprove : CommandElab

Equations

• One or more equations did not get rendered due to their size.