Module studio_run 

What Execute does with a Logic or a Math document, for every surface that runs one.

A Logic document is a ## Theorem block, compiled and handed to the prover, or plain English sentences, each read into logic. A Math document is a ## Theory development, every theorem certified on its own, or kernel statements run in order from a fresh kernel, so each run replaces the last. The front page’s mini Studio runs its examples through these, so it shows what the Studio shows; a Code program runs on interpret_for_ui_baseline, and a Hardware design is read by hardware_report::analyze.

Structs

MathRun

What running a Math document produced: a line per statement, and, when the statements ran through the kernel, the kernel they left behind, whose environment the Studio’s Context panel lists. A ## Theory development certifies its theorems on its own and leaves no kernel.

Enums

LogicRun

What running a Logic document produced.

Functions

run_logic

run_math

Runs a Math document from a fresh kernel, so each run replaces the last rather than piling on.