inductive OperatorDirectory.StateMachine.Err : Type

• NoKey : Err
• NoLower : Err
• NoUpper : Err
• BadActivationTime : PosixTime → PosixTime → Err
• NoTkn : Tokens.Elem.TId → Err
• NotRegistered : OperatorId → Err
• NotActive : OperatorId → Err
• NotRetired : OperatorId → Err
• Retired : OperatorId → Err
• Activation : OperatorId → Err
• WrongBondPenFee : ℕ → ℕ → ℕ → Err
• RetireAct : Err
• RegisterAct : Err
• DeregisterAct : Err
• ActRemAct : Err
• UpdateBondAct : Err
• RecoverBAct : Err
• RetRemAct : Err
• ActList : MOList.Computation.Err → Err
• RetList : MOList.Computation.Err → Err
• RegList : MUList.Computation.Err → Err

instance OperatorDirectory.StateMachine.instReprErr : Repr Err

Equations

• OperatorDirectory.StateMachine.instReprErr = { reprPrec := OperatorDirectory.StateMachine.instReprErr.repr }

def OperatorDirectory.StateMachine.instReprErr.repr : Err → ℕ → Std.Format

Equations

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

def OperatorDirectory.StateMachine.next (p : MidgardParameters) (i : State.ODirActs) (s : State.OperatorDirectory) : ComputationResult Err State.OperatorDirectory

Equations

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