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
Instances For

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

    Equations
    Instances For

      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.
      Instances For

        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.
        Instances For