structure OperatorDirectory.State.OperatorDirectory : Type

• registered : MUList.State.ListST PosixTime
• active : MUList.State.ListST (Option PosixTime)
• retired : MUList.State.ListST (Option PosixTime)

def OperatorDirectory.State.OperatorDirectory.init : OperatorDirectory

Equations

• OperatorDirectory.State.OperatorDirectory.init = { registered := (MUList.State.ListST.init 0).1, active := (MUList.State.ListST.init none).1, retired := (MUList.State.ListST.init none).1 }

inductive OperatorDirectory.State.WitnessStatus : Type

• Active (tkn : Tokens.Elem.TId) : WitnessStatus
• Registered (tkn : Tokens.Elem.TId) : WitnessStatus
• Retired (tkn : Tokens.Elem.TId) : WitnessStatus

inductive OperatorDirectory.State.OperActions : Type

• Activate (toact anchor_reg ret_non act_anch : Tokens.Elem.TId) : OperActions
• Retire (act_node act_anchor ret_anchor : Tokens.Elem.TId) : OperActions
• Register : Tokens.Elem.TId → OperActions
• Deregister : Tokens.Elem.TId → Tokens.Elem.TId → OperActions
• RemoveDuplicateSlashBond : Tokens.Elem.TId → Tokens.Elem.TId → WitnessStatus → OperActions
• ActRemoveOperatorBad : Tokens.Elem.TId → Tokens.Elem.TId → OperActions
• UpdateBondHold : Tokens.Elem.TId → OperActions
• RecoverBond : Tokens.Elem.TId → Tokens.Elem.TId → OperActions
• RetRemoveOperatorBad : Tokens.Elem.TId → Tokens.Elem.TId → OperActions

@[reducible, inline]

abbrev OperatorDirectory.State.ODirActs : Type

Equations

• OperatorDirectory.State.ODirActs = InfoActions OperatorDirectory.State.OperActions