Governance Actions¶
This section defines several concepts and types used to represent governance actions.
{-# OPTIONS --safe #-} open import Ledger.Dijkstra.Specification.Gov.Base module Ledger.Dijkstra.Specification.Gov.Actions (gs : _) (open GovStructure gs) where open import Data.Nat.Properties using (+-0-monoid) open import Data.Rational using (ℚ; 0ℚ; 1ℚ) open import Tactic.Derive.Show open import Ledger.Prelude as P hiding (yes; no) open import Ledger.Core.Specification.ProtocolVersion
Roles and Actions¶
There are three governance roles and actors of role are identified by a type of credential. A governance action is one of the seven types.
data GovRole : Type where CC DRep SPO : GovRole GovRoleCredential : GovRole → Type GovRoleCredential CC = Credential GovRoleCredential DRep = Credential GovRoleCredential SPO = KeyHash data GovActionType : Type where NoConfidence : GovActionType UpdateCommittee : GovActionType NewConstitution : GovActionType TriggerHardFork : GovActionType ChangePParams : GovActionType TreasuryWithdrawal : GovActionType Info : GovActionType GovActionData : GovActionType → Type GovActionData NoConfidence = ⊤ GovActionData UpdateCommittee = (Credential ⇀ Epoch) × ℙ Credential × ℚ GovActionData NewConstitution = DocHash × Maybe ScriptHash GovActionData TriggerHardFork = ProtVer GovActionData ChangePParams = PParamsUpdate GovActionData TreasuryWithdrawal = Withdrawals GovActionData Info = ⊤ record GovAction : Type where constructor ⟦_,_⟧ᵍᵃ field gaType : GovActionType gaData : GovActionData gaType open GovAction public -- Governance actions are uniquely identified by a `GovActionID`. GovActionID : Type GovActionID = TxId × ℕ data Vote : Type where yes no abstain : Vote record GovVoter : Type where constructor ⟦_,_⟧ᵍᵛ field gvRole : GovRole gvCredential : GovRoleCredential gvRole record Anchor : Type where -- context about why a vote was cast in a certain manner field url : String hash : DocHash -- abstract but instantiated with 32-bit hash type record GovVote : Type where field gid : GovActionID voter : GovVoter vote : Vote anchor : Maybe Anchor record GovVotes : Type where -- collects votes cast by members of each of the governance roles field gvCC : Credential ⇀ Vote gvDRep : Credential ⇀ Vote gvSPO : KeyHash ⇀ Vote -- Vote Delegation data VDeleg : Type where vDelegCredential : Credential → VDeleg vDelegAbstain : VDeleg vDelegNoConfidence : VDeleg VoteDelegs : Type VoteDelegs = Credential ⇀ VDeleg -- Hash Protection NeedsHash : GovActionType → Type NeedsHash NoConfidence = GovActionID NeedsHash UpdateCommittee = GovActionID NeedsHash NewConstitution = GovActionID NeedsHash TriggerHardFork = GovActionID NeedsHash ChangePParams = GovActionID NeedsHash TreasuryWithdrawal = ⊤ NeedsHash Info = ⊤ HashProtected : Type → Type HashProtected A = A × GovActionID Policy : Type Policy = Maybe ScriptHash record GovProposal : Type where field action : GovAction prevAction : NeedsHash (gaType action) -- pointer to previous action policy : Policy -- pointer to optional proposal policy deposit : Coin -- to be returned to returnAddr returnAddr : RewardAddress -- reward address; dep returned here when prop is removed anchor : Anchor -- placeholder for further information about the proposal -- state of an individual governance action record GovActionState : Type where field votes : GovVotes returnAddr : RewardAddress expiresIn : Epoch action : GovAction prevAction : NeedsHash (gaType action) -- Governance Helper Functions isGovVoterDRep : GovVoter → Maybe Credential isGovVoterDRep $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{4169}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4176}{\htmlId{4176}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = just c isGovVoterDRep _ = nothing govVoterCredential : GovVoter → Credential govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{4283}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4290}{\htmlId{4290}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = c govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{4322}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4329}{\htmlId{4329}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = c govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{4361}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4368}{\htmlId{4368}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = KeyHashObj kh proposedCC : GovAction → ℙ Credential proposedCC $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{4443}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{4461}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4462}{\htmlId{4462}{\htmlClass{Bound}{\text{x}}}}\, , \,\htmlId{4466}{\htmlClass{Symbol}{\text{\_}}}\, , \,\htmlId{4470}{\htmlClass{Symbol}{\text{\_)}}}\, \end{pmatrix}$ = dom x proposedCC _ = ∅ DReps : Type DReps = Credential ⇀ Epoch
record HasGovActionType (A : Type) : Type where field GovActionTypeOf : A → GovActionType open HasGovActionType ⦃...⦄ public record HasVoteDelegs {a} (A : Type a) : Type a where field VoteDelegsOf : A → VoteDelegs open HasVoteDelegs ⦃...⦄ public record HasGovAction (A : Type) : Type where field GovActionOf : A → GovAction open HasGovAction ⦃...⦄ public record HasGovVoter {a} (A : Type a) : Type a where field GovVoterOf : A → GovVoter open HasGovVoter ⦃...⦄ public record HasGovVotes {a} (A : Type a) : Type a where field GovVotesOf : A → GovVotes open HasGovVotes ⦃...⦄ public record HasVote {a} (A : Type a) : Type a where field VoteOf : A → Vote open HasVote ⦃...⦄ public record HasPolicy {a} (A : Type a) : Type a where field PolicyOf : A → Policy open HasPolicy ⦃...⦄ public record HasDReps {a} (A : Type a) : Type a where field DRepsOf : A → DReps open HasDReps ⦃...⦄ public record HasAnchor {a} (A : Type a) : Type a where field AnchorOf : A → Anchor open HasAnchor ⦃...⦄ public record HasDeposit {a} (A : Type a) : Type a where field DepositOf : A → Coin open HasDeposit ⦃...⦄ public instance HasGovActionType-GovAction : HasGovActionType GovAction HasGovActionType-GovAction .GovActionTypeOf = GovAction.gaType HasCast-GovAction-Sigma : HasCast GovAction (Σ GovActionType GovActionData) HasCast-GovAction-Sigma .cast x = x .gaType , x .gaData HasCast-HashProtected : ∀ {A : Type} → HasCast (HashProtected A) A HasCast-HashProtected .cast = proj₁ HasCast-HashProtected-MaybeScriptHash : HasCast (HashProtected (DocHash × Maybe ScriptHash)) (Maybe ScriptHash) HasCast-HashProtected-MaybeScriptHash .cast = proj₂ ∘ proj₁ HasGovVoter-GovVote : HasGovVoter GovVote HasGovVoter-GovVote .GovVoterOf = GovVote.voter HasVote-GovVote : HasVote GovVote HasVote-GovVote .VoteOf = GovVote.vote HasPolicy-GovProposal : HasPolicy GovProposal HasPolicy-GovProposal .PolicyOf = GovProposal.policy HasAnchor-GovProposal : HasAnchor GovProposal HasAnchor-GovProposal .AnchorOf = GovProposal.anchor HasDeposit-GovProposal : HasDeposit GovProposal HasDeposit-GovProposal .DepositOf = GovProposal.deposit HasGovAction-GovProposal : HasGovAction GovProposal HasGovAction-GovProposal .GovActionOf = GovProposal.action HasGovAction-GovActionState : HasGovAction GovActionState HasGovAction-GovActionState .GovActionOf = GovActionState.action HasGovActionType-GovProposal : HasGovActionType GovProposal HasGovActionType-GovProposal .GovActionTypeOf = GovActionTypeOf ∘ GovActionOf HasGovActionType-GovActionState : HasGovActionType GovActionState HasGovActionType-GovActionState .GovActionTypeOf = GovActionTypeOf ∘ GovActionOf HasGovVotes-GovActionState : HasGovVotes GovActionState HasGovVotes-GovActionState .GovVotesOf = GovActionState.votes HasRewardAddress-GovActionState : HasRewardAddress GovActionState HasRewardAddress-GovActionState .RewardAddressOf = GovActionState.returnAddr HasRewardAddress-GovProposal : HasRewardAddress GovProposal HasRewardAddress-GovProposal .RewardAddressOf = GovProposal.returnAddr unquoteDecl Show-GovRole = derive-Show [ (quote GovRole , Show-GovRole) ] unquoteDecl DecEq-GovActionType = derive-DecEq ((quote GovActionType , DecEq-GovActionType) ∷ []) unquoteDecl DecEq-GovRole = derive-DecEq ((quote GovRole , DecEq-GovRole) ∷ []) unquoteDecl DecEq-Vote = derive-DecEq ((quote Vote , DecEq-Vote) ∷ []) unquoteDecl DecEq-VDeleg = derive-DecEq ((quote VDeleg , DecEq-VDeleg) ∷ []) DecEq-GovVoter : DecEq GovVoter DecEq-GovVoter ._≟_ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8183}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8190}{\htmlId{8190}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8198}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8205}{\htmlId{8205}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}$ with c ≟ c' ... | P.yes p = P.yes (cong $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8260}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8242}{\htmlId{8269}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8270}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{8274}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8278}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8280}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8285}{\htmlId{8285}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8288}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8290}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8295}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8298}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8300}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8305}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8285}{\htmlId{8307}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8310}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8314}{\htmlClass{Symbol}{\text{})}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8319}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8334}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8335}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8341}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8348}{\htmlId{8348}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8356}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8363}{\htmlId{8363}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8370}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8372}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8377}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8379}{\htmlClass{Symbol}{\text{()}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8384}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8399}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8400}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8406}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8413}{\htmlId{8413}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8421}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8428}{\htmlId{8428}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8435}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8437}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8442}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8444}{\htmlClass{Symbol}{\text{()}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8449}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8464}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8465}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8471}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8478}{\htmlId{8478}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8486}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8493}{\htmlId{8493}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8500}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8502}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8507}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8509}{\htmlClass{Symbol}{\text{()}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8514}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8529}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8530}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8536}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8543}{\htmlId{8543}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8551}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8558}{\htmlId{8558}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8569}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8543}{\htmlId{8574}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8576}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8558}{\htmlId{8578}{\htmlClass{Bound}{\text{c'}}}}\, \,\htmlId{8583}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8587}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8589}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8595}{\htmlId{8595}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8597}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8599}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8605}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8606}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8613}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8595}{\htmlId{8624}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8625}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{8629}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8633}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8635}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8640}{\htmlId{8640}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8643}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8645}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8650}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8653}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8655}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8660}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8640}{\htmlId{8662}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8665}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8669}{\htmlClass{Symbol}{\text{})}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8674}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8689}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8690}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8696}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8703}{\htmlId{8703}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8711}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8718}{\htmlId{8718}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8725}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8727}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8732}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8734}{\htmlClass{Symbol}{\text{()}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8739}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8754}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8755}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8761}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8768}{\htmlId{8768}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8776}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8783}{\htmlId{8783}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8790}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8792}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8797}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8799}{\htmlClass{Symbol}{\text{()}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8804}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8819}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8820}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8826}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8833}{\htmlId{8833}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8841}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8848}{\htmlId{8848}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8855}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8857}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8862}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8864}{\htmlClass{Symbol}{\text{()}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8127}{\htmlId{8869}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8884}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8885}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8891}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8898}{\htmlId{8898}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8906}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8913}{\htmlId{8913}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8924}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8898}{\htmlId{8929}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8931}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8913}{\htmlId{8933}{\htmlClass{Bound}{\text{c'}}}}\, \,\htmlId{8938}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8942}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8944}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8950}{\htmlId{8950}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8952}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8954}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8960}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8961}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8968}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8950}{\htmlId{8978}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8979}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{8983}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8987}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8989}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8994}{\htmlId{8994}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8997}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8999}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{9004}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{9007}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{9009}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{9014}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8994}{\htmlId{9016}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{9019}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{9023}{\htmlClass{Symbol}{\text{})}}}\, \,\htmlId{9029}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9041}{\htmlId{9041}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{9057}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{9059}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9074}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{9076}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{9077}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2336}{\htmlId{9083}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9041}{\htmlId{9093}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{9108}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9110}{\htmlClass{Function Operator}{\text{]}}}}\, \,\htmlId{9114}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9126}{\htmlId{9126}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{9138}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{9140}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9152}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{9154}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{9155}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2697}{\htmlId{9161}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9126}{\htmlId{9170}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{9181}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9183}{\htmlClass{Function Operator}{\text{]}}}}\, \,\htmlId{9187}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9199}{\htmlId{9199}{\htmlClass{Function}{\text{DecEq-Anchor}}}}\, \,\htmlId{9219}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.DecEq.html#5150}{\htmlId{9221}{\htmlClass{Function}{\text{derive-DecEq}}}}\, \,\htmlId{9234}{\htmlClass{Symbol}{\text{((}}}\,\,\htmlId{9236}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2151}{\htmlId{9242}{\htmlClass{Record}{\text{Anchor}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9199}{\htmlId{9252}{\htmlClass{Function}{\text{DecEq-Anchor}}}}\,\,\htmlId{9264}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Agda.Builtin.List.html#199}{\htmlId{9267}{\htmlClass{InductiveConstructor Operator}{\text{∷}}}}\, \,\href{Agda.Builtin.List.html#184}{\htmlId{9269}{\htmlClass{InductiveConstructor}{\text{[]}}}}\,\,\htmlId{9271}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9274}{\htmlId{9274}{\htmlClass{Function}{\text{==-Set}}}}\, \,\htmlId{9281}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{9283}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{9285}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9286}{\htmlId{9286}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{9287}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{9289}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9291}{\htmlId{9291}{\htmlClass{Bound}{\text{dA}}}}\, \,\htmlId{9294}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Class.DecEq.Core.html#126}{\htmlId{9296}{\htmlClass{Record}{\text{DecEq}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9286}{\htmlId{9302}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9304}{\htmlClass{Symbol}{\text{⦄}}}\, \,\htmlId{9306}{\htmlClass{Symbol}{\text{→}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#488}{\htmlId{9308}{\htmlClass{Function Operator}{\text{ℙ}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9286}{\htmlId{9310}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9312}{\htmlClass{Symbol}{\text{→}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#488}{\htmlId{9314}{\htmlClass{Function Operator}{\text{ℙ}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9286}{\htmlId{9316}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9318}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{9320}{\htmlClass{Datatype}{\text{Bool}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9274}{\htmlId{9325}{\htmlClass{Function}{\text{==-Set}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9332}{\htmlId{9332}{\htmlClass{Bound}{\text{xs}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9335}{\htmlId{9335}{\htmlClass{Bound}{\text{ys}}}}\, \,\htmlId{9338}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Data.Bool.ListAction.html#927}{\htmlId{9344}{\htmlClass{Function}{\text{all}}}}\, \,\htmlId{9348}{\htmlClass{Symbol}{\text{(λ}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9351}{\htmlId{9351}{\htmlClass{Bound}{\text{x}}}}\, \,\htmlId{9353}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Relation.Nullary.Decidable.Core.html#5031}{\htmlId{9355}{\htmlClass{Function Operator}{\text{⌊}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9351}{\htmlId{9357}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Axiom.Set.html#11038}{\htmlId{9359}{\htmlClass{Function Operator}{\text{∈?}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9335}{\htmlId{9362}{\htmlClass{Bound}{\text{ys}}}}\, \,\href{Relation.Nullary.Decidable.Core.html#5031}{\htmlId{9365}{\htmlClass{Function Operator}{\text{⌋}}}}\,\,\htmlId{9366}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9368}{\htmlClass{Symbol}{\text{(}}}\,\,\href{abstract-set-theory.FiniteSetTheory.html#2617}{\htmlId{9369}{\htmlClass{Function}{\text{setToList}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9332}{\htmlId{9379}{\htmlClass{Bound}{\text{xs}}}}\,\,\htmlId{9381}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{9383}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\href{Data.Bool.ListAction.html#927}{\htmlId{9389}{\htmlClass{Function}{\text{all}}}}\, \,\htmlId{9393}{\htmlClass{Symbol}{\text{(λ}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9396}{\htmlId{9396}{\htmlClass{Bound}{\text{y}}}}\, \,\htmlId{9398}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Relation.Nullary.Decidable.Core.html#5031}{\htmlId{9400}{\htmlClass{Function Operator}{\text{⌊}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9396}{\htmlId{9402}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Axiom.Set.html#11038}{\htmlId{9404}{\htmlClass{Function Operator}{\text{∈?}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9332}{\htmlId{9407}{\htmlClass{Bound}{\text{xs}}}}\, \,\href{Relation.Nullary.Decidable.Core.html#5031}{\htmlId{9410}{\htmlClass{Function Operator}{\text{⌋}}}}\,\,\htmlId{9411}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9413}{\htmlClass{Symbol}{\text{(}}}\,\,\href{abstract-set-theory.FiniteSetTheory.html#2617}{\htmlId{9414}{\htmlClass{Function}{\text{setToList}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9335}{\htmlId{9424}{\htmlClass{Bound}{\text{ys}}}}\,\,\htmlId{9426}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9429}{\htmlId{9429}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\htmlId{9446}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{9448}{\htmlClass{Symbol}{\text{∀}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9450}{\htmlId{9450}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9452}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1314}{\htmlId{9454}{\htmlClass{Function}{\text{GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9450}{\htmlId{9468}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9470}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1314}{\htmlId{9472}{\htmlClass{Function}{\text{GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9450}{\htmlId{9486}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9488}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{9490}{\htmlClass{Datatype}{\text{Bool}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9429}{\htmlId{9495}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{9512}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \,\htmlId{9525}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9527}{\htmlClass{Function Operator}{\text{\_==\_}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9429}{\htmlId{9532}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{9549}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \,\htmlId{9565}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9566}{\htmlId{9566}{\htmlClass{Bound}{\text{m0}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9571}{\htmlId{9571}{\htmlClass{Bound}{\text{s0}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9576}{\htmlId{9576}{\htmlClass{Bound}{\text{q0}}}}\,\,\htmlId{9578}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9580}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9581}{\htmlId{9581}{\htmlClass{Bound}{\text{m1}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9586}{\htmlId{9586}{\htmlClass{Bound}{\text{s1}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9591}{\htmlId{9591}{\htmlClass{Bound}{\text{q1}}}}\,\,\htmlId{9593}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9595}{\htmlClass{Symbol}{\text{=}}}\, \,\htmlId{9601}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9274}{\htmlId{9602}{\htmlClass{Function}{\text{==-Set}}}}\, \,\htmlId{9609}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9566}{\htmlId{9610}{\htmlClass{Bound}{\text{m0}}}}\, \,\href{Axiom.Set.Map.html#2293}{\htmlId{9613}{\htmlClass{Function Operator}{\text{ˢ}}}}\,\,\htmlId{9614}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9616}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9581}{\htmlId{9617}{\htmlClass{Bound}{\text{m1}}}}\, \,\href{Axiom.Set.Map.html#2293}{\htmlId{9620}{\htmlClass{Function Operator}{\text{ˢ}}}}\,\,\htmlId{9621}{\htmlClass{Symbol}{\text{))}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{9624}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{9626}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9571}{\htmlId{9627}{\htmlClass{Bound}{\text{s0}}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9630}{\htmlClass{Function Operator}{\text{==}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9586}{\htmlId{9633}{\htmlClass{Bound}{\text{s1}}}}\,\,\htmlId{9635}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{9637}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{9639}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9576}{\htmlId{9640}{\htmlClass{Bound}{\text{q0}}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9643}{\htmlClass{Function Operator}{\text{==}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9591}{\htmlId{9646}{\htmlClass{Bound}{\text{q1}}}}\,\,\htmlId{9648}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9429}{\htmlId{9650}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{9667}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \,\htmlId{9683}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9685}{\htmlClass{Function Operator}{\text{\_==\_}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9429}{\htmlId{9690}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{9707}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \,\htmlId{9723}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9725}{\htmlClass{Function Operator}{\text{\_==\_}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9429}{\htmlId{9730}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{9747}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \,\htmlId{9761}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9763}{\htmlClass{Function Operator}{\text{\_==\_}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9429}{\htmlId{9768}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{9785}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9804}{\htmlId{9804}{\htmlClass{Bound}{\text{w0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9807}{\htmlId{9807}{\htmlClass{Bound}{\text{w1}}}}\, \,\htmlId{9810}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9274}{\htmlId{9812}{\htmlClass{Function}{\text{==-Set}}}}\, \,\htmlId{9819}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9804}{\htmlId{9820}{\htmlClass{Bound}{\text{w0}}}}\, \,\href{Axiom.Set.Map.html#2293}{\htmlId{9823}{\htmlClass{Function Operator}{\text{ˢ}}}}\,\,\htmlId{9824}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9826}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9807}{\htmlId{9827}{\htmlClass{Bound}{\text{w1}}}}\, \,\href{Axiom.Set.Map.html#2293}{\htmlId{9830}{\htmlClass{Function Operator}{\text{ˢ}}}}\,\,\htmlId{9831}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9429}{\htmlId{9833}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{9850}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \,\htmlId{9855}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9857}{\htmlClass{Function Operator}{\text{\_==\_}}}}\, \,\htmlId{9863}{\htmlClass{Comment}{\text{-- See note "GovAction and GovProposal equality"}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9912}{\htmlId{9912}{\htmlClass{Function}{\text{==-GovAction}}}}\, \,\htmlId{9925}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1716}{\htmlId{9927}{\htmlClass{Record}{\text{GovAction}}}}\, \,\htmlId{9937}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1716}{\htmlId{9939}{\htmlClass{Record}{\text{GovAction}}}}\, \,\htmlId{9949}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{9951}{\htmlClass{Datatype}{\text{Bool}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9912}{\htmlId{9956}{\htmlClass{Function}{\text{==-GovAction}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9971}{\htmlId{9971}{\htmlClass{Bound}{\text{t0}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9976}{\htmlId{9976}{\htmlClass{Bound}{\text{d0}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9985}{\htmlId{9985}{\htmlClass{Bound}{\text{t1}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9990}{\htmlId{9990}{\htmlClass{Bound}{\text{d1}}}}\, \end{pmatrix} \,\htmlId{10001}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9971}{\htmlId{10006}{\htmlClass{Bound}{\text{t0}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10009}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9985}{\htmlId{10011}{\htmlClass{Bound}{\text{t1}}}}\, \,\htmlId{10014}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{10018}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{10020}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{10026}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{10031}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9429}{\htmlId{10033}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\htmlId{10050}{\htmlClass{Bound}{\text{t1}}}\, \,\htmlId{10053}{\htmlClass{Bound}{\text{d0}}}\, \,\htmlId{10056}{\htmlClass{Bound}{\text{d1}}}\, \,\htmlId{10059}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{10063}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10065}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{10070}{\htmlClass{Symbol}{\text{\_}}}\, \,\htmlId{10072}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Bool.html#192}{\htmlId{10074}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10081}{\htmlId{10081}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10097}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{10099}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{10101}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10102}{\htmlId{10102}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{10103}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10105}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Class.DecEq.Core.html#126}{\htmlId{10107}{\htmlClass{Record}{\text{DecEq}}}}\, \,\htmlId{10113}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2894}{\htmlId{10114}{\htmlClass{Function}{\text{NeedsHash}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10102}{\htmlId{10124}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{10125}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10081}{\htmlId{10127}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10143}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{10144}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,\,\htmlId{10156}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10158}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10159}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10163}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10165}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10169}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2346}{\htmlId{10171}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{10180}{\htmlClass{Symbol}{\text{⦄}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10081}{\htmlId{10182}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10198}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{10199}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,\,\htmlId{10214}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10216}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10217}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10221}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10223}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10227}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2346}{\htmlId{10229}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{10238}{\htmlClass{Symbol}{\text{⦄}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10081}{\htmlId{10240}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10256}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{10257}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,\,\htmlId{10272}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10274}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10275}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10279}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10281}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10285}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2346}{\htmlId{10287}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{10296}{\htmlClass{Symbol}{\text{⦄}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10081}{\htmlId{10298}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10314}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{10315}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,\,\htmlId{10330}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10332}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10333}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10337}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10339}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10343}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2346}{\htmlId{10345}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{10354}{\htmlClass{Symbol}{\text{⦄}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10081}{\htmlId{10356}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10372}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{10373}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,\,\htmlId{10386}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10388}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10389}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10393}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10395}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10399}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2346}{\htmlId{10401}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{10410}{\htmlClass{Symbol}{\text{⦄}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10081}{\htmlId{10412}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10428}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{10429}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,\,\htmlId{10447}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10449}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10450}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10454}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10456}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10460}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Class.DecEq.Instances.html#193}{\htmlId{10462}{\htmlClass{Function}{\text{DecEq-⊤}}}}\, \,\htmlId{10470}{\htmlClass{Symbol}{\text{⦄}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10081}{\htmlId{10472}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10488}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{10489}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,\,\htmlId{10493}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10495}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10496}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10500}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10502}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10506}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Class.DecEq.Instances.html#193}{\htmlId{10508}{\htmlClass{Function}{\text{DecEq-⊤}}}}\, \,\htmlId{10516}{\htmlClass{Symbol}{\text{⦄}}}\, \,\htmlId{10519}{\htmlClass{Comment}{\text{-- See note "GovAction and GovProposal equality"}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10568}{\htmlId{10568}{\htmlClass{Function}{\text{==-GovProposal}}}}\, \,\htmlId{10583}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3327}{\htmlId{10585}{\htmlClass{Record}{\text{GovProposal}}}}\, \,\htmlId{10597}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3327}{\htmlId{10599}{\htmlClass{Record}{\text{GovProposal}}}}\, \,\htmlId{10611}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{10613}{\htmlClass{Datatype}{\text{Bool}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10568}{\htmlId{10618}{\htmlClass{Function}{\text{==-GovProposal}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10633}{\htmlId{10633}{\htmlClass{Bound Operator}{\text{\_gp0}}}}\,\,\htmlId{10637}{\htmlClass{Symbol}{\text{@(}}}\,\,\htmlId{10639}{\htmlClass{InductiveConstructor}{\text{GovProposal.constructor}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10663}{\htmlId{10663}{\htmlClass{Bound}{\text{a0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10666}{\htmlId{10666}{\htmlClass{Bound}{\text{b0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10669}{\htmlId{10669}{\htmlClass{Bound}{\text{c0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10672}{\htmlId{10672}{\htmlClass{Bound}{\text{d0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10675}{\htmlId{10675}{\htmlClass{Bound}{\text{e0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10678}{\htmlId{10678}{\htmlClass{Bound}{\text{f0}}}}\,\,\htmlId{10680}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10697}{\htmlId{10697}{\htmlClass{Bound Operator}{\text{\_gp1}}}}\,\,\htmlId{10701}{\htmlClass{Symbol}{\text{@(}}}\,\,\htmlId{10703}{\htmlClass{InductiveConstructor}{\text{GovProposal.constructor}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10727}{\htmlId{10727}{\htmlClass{Bound}{\text{a1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10730}{\htmlId{10730}{\htmlClass{Bound}{\text{b1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10733}{\htmlId{10733}{\htmlClass{Bound}{\text{c1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10736}{\htmlId{10736}{\htmlClass{Bound}{\text{d1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10739}{\htmlId{10739}{\htmlClass{Bound}{\text{e1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10742}{\htmlId{10742}{\htmlClass{Bound}{\text{f1}}}}\,\,\htmlId{10744}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{10748}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1773}{\htmlId{10753}{\htmlClass{Field}{\text{GovAction.gaType}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10663}{\htmlId{10770}{\htmlClass{Bound}{\text{a0}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10773}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1773}{\htmlId{10775}{\htmlClass{Field}{\text{GovAction.gaType}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10727}{\htmlId{10792}{\htmlClass{Bound}{\text{a1}}}}\, \,\htmlId{10795}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{10799}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{10801}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{10807}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{10812}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9912}{\htmlId{10818}{\htmlClass{Function}{\text{==-GovAction}}}}\, \,\htmlId{10831}{\htmlClass{Bound}{\text{a0}}}\, \,\htmlId{10834}{\htmlClass{Bound}{\text{a1}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{10841}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10843}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10844}{\htmlClass{Bound}{\text{b0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10847}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10850}{\htmlClass{Bound}{\text{b1}}}\,\,\htmlId{10852}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{10858}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10860}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10861}{\htmlClass{Bound}{\text{c0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10864}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10867}{\htmlClass{Bound}{\text{c1}}}\,\,\htmlId{10869}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{10875}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10877}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10878}{\htmlClass{Bound}{\text{d0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10881}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10884}{\htmlClass{Bound}{\text{d1}}}\,\,\htmlId{10886}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{10892}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10894}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10895}{\htmlClass{Bound}{\text{e0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10898}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10901}{\htmlClass{Bound}{\text{e1}}}\,\,\htmlId{10903}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{10909}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10911}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10912}{\htmlClass{Bound}{\text{f0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10915}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10918}{\htmlClass{Bound}{\text{f1}}}\,\,\htmlId{10920}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{10924}{\htmlClass{Keyword}{\text{where}}}\, \,\htmlId{10934}{\htmlClass{Keyword}{\text{open}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3327}{\htmlId{10939}{\htmlClass{Module}{\text{GovProposal}}}}\, \,\htmlId{10955}{\htmlClass{Keyword}{\text{instance}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10964}{\htmlId{10964}{\htmlClass{Function}{\text{\_}}}}\, \,\htmlId{10966}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10081}{\htmlId{10968}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10984}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{10988}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10990}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{10995}{\htmlClass{Symbol}{\text{\_}}}\, \,\htmlId{10997}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Bool.html#192}{\htmlId{10999}{\htmlClass{InductiveConstructor}{\text{false}}}}\,
-- return the DReps of A that expire in epoch e or later activeInEpoch : Epoch → Credential × Epoch → Type activeInEpoch e (_ , expEpoch) = e ≤ expEpoch activeDRepsOf : {A : Type} ⦃ _ : HasDReps A ⦄ → A → Epoch → DReps activeDRepsOf a e = filterᵐ (activeInEpoch e) (DRepsOf a)