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

• run_cmd doSeq command which 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.

• run_tac doSeq tactic which executes code in TacticM Unit.

• by_elab doSeq term which executes code in TermElabM Expr to produce an expression.

def Mathlib.RunCmd.runCmd : Lean.ParserDescr

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.

def Mathlib.RunCmd.runTac : Lean.ParserDescr

The run_tac doSeq tactic executes code in TacticM Unit.

def Mathlib.RunCmd.byElab : Lean.ParserDescr

• The by_elab doSeq expression runs the doSeq as a TermElabM Expr to synthesize the expression.
• by_elab fun expectedType? ↦ do doSeq receives the expected type (an Option Expr) as well.

def Mathlib.RunCmd.elabRunElab : Lean.Elab.Term.TermElab

Elaborator for by_elab.