Defines commands to compile and execute a command / term / tactic on the spot:
-
run_cmd doSeq
command which executes code inCommandElabM 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 inTacticM Unit
. -
by_elab doSeq
term which executes code inTermElabM Expr
to produce an expression.
The run_tac doSeq
tactic executes code in TacticM Unit
.
Instances For
- The
by_elab doSeq
expression runs thedoSeq
as aTermElabM Expr
to synthesize the expression. by_elab fun expectedType? ↦ do doSeq
receives the expected type (anOption Expr
) as well.