Documentation

Batteries.Lean.Meta.SavedState

Run the action x in state s. Returns the result of x and the state after x was executed. The global state remains unchanged.

Equations

Run the action x in state s. Returns the result of x. The global state remains unchanged.

Equations

Returns the mvars that are not declared in preState, but declared and unassigned in postState. Delayed-assigned mvars are considered assigned.

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

Returns the mvars that are declared but unassigned in preState, and assigned in postState. Delayed-assigned mvars are considered assigned.

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