Documentation

Mathlib.Tactic.RunCmd

Defines commands to compile and execute a command / term / tactic on the spot:

The run_cmd doSeq command executes code in CommandElabM Unit. This is almost the same as #eval show CommandElabM Unit from do doSeq, except that it doesn't print an empty diagnostic.

Equations

The run_tac doSeq tactic executes code in TacticM Unit.

Equations
  • One or more equations did not get rendered due to their size.
  • The by_elab doSeq expression runs the doSeq as a TermElabM Expr to synthesize the expression.
  • by_elab fun expectedType? ↦ do doSeq↦ do doSeq receives the expected type (an Option Expr) as well.
Equations

Elaborator for by_elab.

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