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 Std.Tactic.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

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

def Std.Tactic.RunCmd.runElab : Lean.ParserDescr

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

Equations

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

def Std.Tactic.RunCmd.runMeta : Lean.ParserDescr

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

(This is effectively a synonym for run_elab.)

Equations

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

def Std.Tactic.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.

def Std.Tactic.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.

Equations

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

def Std.Tactic.RunCmd.elabRunElab : Lean.Elab.Term.TermElab

Elaborator for by_elab.

Equations

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