inductive MOList.Computation.Err : Type

• UList : MUList.Computation.Err → Err
• MissingTnk : Tokens.Elem.TId → Err
• InvalidNonMemApp : MUList.State.Key → Option MUList.State.Key → Err
• InvalidNonMemPre : MUList.State.Key → Option MUList.State.Key → Err
• InvalidNonMemIns : MUList.State.Key → Option MUList.State.Key → Err

instance MOList.Computation.instReprErr : Repr Err

Equations

• MOList.Computation.instReprErr = { reprPrec := MOList.Computation.instReprErr.repr }

def MOList.Computation.instReprErr.repr : Err → ℕ → Std.Format

Equations

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

def MOList.Computation.next {α : Type} (a : State.Actions α) (s : MUList.State.ListST α) : ComputationResult Err (MUList.State.ListST α)

Equations

• One or more equations did not get rendered due to their size.
• MOList.Computation.next (MOList.State.Actions.ModifyData t d) s = ComputationResult.merr MOList.Computation.Err.UList (MUList.Computation.next (MUList.State.Actions.ModifyData t d) s)
• MOList.Computation.next (MOList.State.Actions.Remove r a_2) s = ComputationResult.merr MOList.Computation.Err.UList (MUList.Computation.next (MUList.State.Actions.Remove r a_2) s)