Lift an action in CommandElabM
into CoreM
, updating the traces and the environment.
This does not preserve things like open
and namespace
declarations.
Equations
- One or more equations did not get rendered due to their size.
Std.Lean.Command
Lift an action in CommandElabM
into CoreM
, updating the traces and the environment.
This does not preserve things like open
and namespace
declarations.