Documentation

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.

Instances For

    Evaluate any set_option in commands before the given stx, and pass the inner stx with the updated environment to the continuation k.