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.

ink

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.

Equations

• Mathlib.RunCmd.runCmd = Lean.ParserDescr.node `Mathlib.RunCmd.runCmd 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "run_cmd ") (Lean.ParserDescr.const `doSeq))

ink

def Mathlib.RunCmd.runTac : Lean.ParserDescr

The run_tac doSeq tactic executes code in TacticM Unit.

Equations

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

ink

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↦ do doSeq receives the expected type (an Option Expr) as well.

Equations

• Mathlib.RunCmd.byElab = Lean.ParserDescr.node `Mathlib.RunCmd.byElab 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "by_elab") (Lean.ParserDescr.const `doSeq))

ink

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

Elaborator for by_elab.

Equations

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