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) deposit : Coin -- Governance Helper Functions isGovVoterDRep : GovVoter → Maybe Credential isGovVoterDRep $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{4192}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4199}{\htmlId{4199}{\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{4306}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4313}{\htmlId{4313}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = c govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{4345}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4352}{\htmlId{4352}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = c govVoterCredential $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{4384}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4391}{\htmlId{4391}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = KeyHashObj kh proposedCC : GovAction → ℙ Credential proposedCC $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{4466}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{4484}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4485}{\htmlId{4485}{\htmlClass{Bound}{\text{x}}}}\, , \,\htmlId{4489}{\htmlClass{Symbol}{\text{\_}}}\, , \,\htmlId{4493}{\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{8206}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8213}{\htmlId{8213}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8221}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8228}{\htmlId{8228}{\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{8283}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8265}{\htmlId{8292}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8293}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{8297}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8301}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8303}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8308}{\htmlId{8308}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8311}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8313}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8318}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8321}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8323}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8328}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8308}{\htmlId{8330}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8333}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8337}{\htmlClass{Symbol}{\text{})}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8150}{\htmlId{8342}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8357}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8358}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8364}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8371}{\htmlId{8371}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8379}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8386}{\htmlId{8386}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8393}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8395}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8400}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8402}{\htmlClass{Symbol}{\text{()}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8150}{\htmlId{8407}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8422}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8423}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8429}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8436}{\htmlId{8436}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8444}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8451}{\htmlId{8451}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8458}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8460}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8465}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8467}{\htmlClass{Symbol}{\text{()}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8150}{\htmlId{8472}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8487}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8488}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8494}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8501}{\htmlId{8501}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8509}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8516}{\htmlId{8516}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8523}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8525}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8530}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8532}{\htmlClass{Symbol}{\text{()}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8150}{\htmlId{8537}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8552}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8553}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8559}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8566}{\htmlId{8566}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8574}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8581}{\htmlId{8581}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8592}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8566}{\htmlId{8597}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8599}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8581}{\htmlId{8601}{\htmlClass{Bound}{\text{c'}}}}\, \,\htmlId{8606}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8610}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8612}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8618}{\htmlId{8618}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8620}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8622}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8628}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8629}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8636}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8618}{\htmlId{8647}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{8648}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{8652}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8656}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8658}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8663}{\htmlId{8663}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{8666}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8668}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8673}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{8676}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8678}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8683}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8663}{\htmlId{8685}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8688}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{8692}{\htmlClass{Symbol}{\text{})}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8150}{\htmlId{8697}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8712}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8713}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8719}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8726}{\htmlId{8726}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8734}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8741}{\htmlId{8741}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8748}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8750}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8755}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8757}{\htmlClass{Symbol}{\text{()}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8150}{\htmlId{8762}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8777}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8778}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8784}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8791}{\htmlId{8791}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{8799}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8806}{\htmlId{8806}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8813}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8815}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8820}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8822}{\htmlClass{Symbol}{\text{()}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8150}{\htmlId{8827}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8842}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8843}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8849}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8856}{\htmlId{8856}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{8864}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8871}{\htmlId{8871}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8878}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8880}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8885}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{8887}{\htmlClass{Symbol}{\text{()}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8150}{\htmlId{8892}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{8907}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{8908}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8914}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8921}{\htmlId{8921}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8929}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8936}{\htmlId{8936}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{8947}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8921}{\htmlId{8952}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8954}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8936}{\htmlId{8956}{\htmlClass{Bound}{\text{c'}}}}\, \,\htmlId{8961}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8965}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8967}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8973}{\htmlId{8973}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{8975}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8977}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{8983}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8984}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{8991}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#8973}{\htmlId{9001}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{9002}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9006}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{9010}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{9012}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9017}{\htmlId{9017}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{9020}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{9022}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{9027}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{9030}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{9032}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{9037}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9017}{\htmlId{9039}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{9042}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{9046}{\htmlClass{Symbol}{\text{})}}}\, \,\htmlId{9052}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9064}{\htmlId{9064}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{9080}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{9082}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9097}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{9099}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{9100}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2336}{\htmlId{9106}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9064}{\htmlId{9116}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{9131}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9133}{\htmlClass{Function Operator}{\text{]}}}}\, \,\htmlId{9137}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9149}{\htmlId{9149}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{9161}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{9163}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9175}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{9177}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{9178}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2697}{\htmlId{9184}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9149}{\htmlId{9193}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{9204}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{9206}{\htmlClass{Function Operator}{\text{]}}}}\, \,\htmlId{9210}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9222}{\htmlId{9222}{\htmlClass{Function}{\text{DecEq-Anchor}}}}\, \,\htmlId{9242}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.DecEq.html#5150}{\htmlId{9244}{\htmlClass{Function}{\text{derive-DecEq}}}}\, \,\htmlId{9257}{\htmlClass{Symbol}{\text{((}}}\,\,\htmlId{9259}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2151}{\htmlId{9265}{\htmlClass{Record}{\text{Anchor}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9222}{\htmlId{9275}{\htmlClass{Function}{\text{DecEq-Anchor}}}}\,\,\htmlId{9287}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Agda.Builtin.List.html#199}{\htmlId{9290}{\htmlClass{InductiveConstructor Operator}{\text{∷}}}}\, \,\href{Agda.Builtin.List.html#184}{\htmlId{9292}{\htmlClass{InductiveConstructor}{\text{[]}}}}\,\,\htmlId{9294}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9297}{\htmlId{9297}{\htmlClass{Function}{\text{==-Set}}}}\, \,\htmlId{9304}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{9306}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{9308}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9309}{\htmlId{9309}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{9310}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{9312}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9314}{\htmlId{9314}{\htmlClass{Bound}{\text{dA}}}}\, \,\htmlId{9317}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Class.DecEq.Core.html#126}{\htmlId{9319}{\htmlClass{Record}{\text{DecEq}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9309}{\htmlId{9325}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9327}{\htmlClass{Symbol}{\text{⦄}}}\, \,\htmlId{9329}{\htmlClass{Symbol}{\text{→}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#488}{\htmlId{9331}{\htmlClass{Function Operator}{\text{ℙ}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9309}{\htmlId{9333}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9335}{\htmlClass{Symbol}{\text{→}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#488}{\htmlId{9337}{\htmlClass{Function Operator}{\text{ℙ}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9309}{\htmlId{9339}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9341}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{9343}{\htmlClass{Datatype}{\text{Bool}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9297}{\htmlId{9348}{\htmlClass{Function}{\text{==-Set}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9355}{\htmlId{9355}{\htmlClass{Bound}{\text{xs}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9358}{\htmlId{9358}{\htmlClass{Bound}{\text{ys}}}}\, \,\htmlId{9361}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Data.Bool.ListAction.html#927}{\htmlId{9367}{\htmlClass{Function}{\text{all}}}}\, \,\htmlId{9371}{\htmlClass{Symbol}{\text{(λ}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9374}{\htmlId{9374}{\htmlClass{Bound}{\text{x}}}}\, \,\htmlId{9376}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Relation.Nullary.Decidable.Core.html#5031}{\htmlId{9378}{\htmlClass{Function Operator}{\text{⌊}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9374}{\htmlId{9380}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Axiom.Set.html#11038}{\htmlId{9382}{\htmlClass{Function Operator}{\text{∈?}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9358}{\htmlId{9385}{\htmlClass{Bound}{\text{ys}}}}\, \,\href{Relation.Nullary.Decidable.Core.html#5031}{\htmlId{9388}{\htmlClass{Function Operator}{\text{⌋}}}}\,\,\htmlId{9389}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9391}{\htmlClass{Symbol}{\text{(}}}\,\,\href{abstract-set-theory.FiniteSetTheory.html#2617}{\htmlId{9392}{\htmlClass{Function}{\text{setToList}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9355}{\htmlId{9402}{\htmlClass{Bound}{\text{xs}}}}\,\,\htmlId{9404}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{9406}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\href{Data.Bool.ListAction.html#927}{\htmlId{9412}{\htmlClass{Function}{\text{all}}}}\, \,\htmlId{9416}{\htmlClass{Symbol}{\text{(λ}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9419}{\htmlId{9419}{\htmlClass{Bound}{\text{y}}}}\, \,\htmlId{9421}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Relation.Nullary.Decidable.Core.html#5031}{\htmlId{9423}{\htmlClass{Function Operator}{\text{⌊}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9419}{\htmlId{9425}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Axiom.Set.html#11038}{\htmlId{9427}{\htmlClass{Function Operator}{\text{∈?}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9355}{\htmlId{9430}{\htmlClass{Bound}{\text{xs}}}}\, \,\href{Relation.Nullary.Decidable.Core.html#5031}{\htmlId{9433}{\htmlClass{Function Operator}{\text{⌋}}}}\,\,\htmlId{9434}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9436}{\htmlClass{Symbol}{\text{(}}}\,\,\href{abstract-set-theory.FiniteSetTheory.html#2617}{\htmlId{9437}{\htmlClass{Function}{\text{setToList}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9358}{\htmlId{9447}{\htmlClass{Bound}{\text{ys}}}}\,\,\htmlId{9449}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9452}{\htmlId{9452}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\htmlId{9469}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{9471}{\htmlClass{Symbol}{\text{∀}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9473}{\htmlId{9473}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9475}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1314}{\htmlId{9477}{\htmlClass{Function}{\text{GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9473}{\htmlId{9491}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9493}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1314}{\htmlId{9495}{\htmlClass{Function}{\text{GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9473}{\htmlId{9509}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9511}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{9513}{\htmlClass{Datatype}{\text{Bool}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9452}{\htmlId{9518}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{9535}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \,\htmlId{9548}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9550}{\htmlClass{Function Operator}{\text{\_==\_}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9452}{\htmlId{9555}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{9572}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \,\htmlId{9588}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9589}{\htmlId{9589}{\htmlClass{Bound}{\text{m0}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9594}{\htmlId{9594}{\htmlClass{Bound}{\text{s0}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9599}{\htmlId{9599}{\htmlClass{Bound}{\text{q0}}}}\,\,\htmlId{9601}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9603}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9604}{\htmlId{9604}{\htmlClass{Bound}{\text{m1}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9609}{\htmlId{9609}{\htmlClass{Bound}{\text{s1}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9614}{\htmlId{9614}{\htmlClass{Bound}{\text{q1}}}}\,\,\htmlId{9616}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9618}{\htmlClass{Symbol}{\text{=}}}\, \,\htmlId{9624}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9297}{\htmlId{9625}{\htmlClass{Function}{\text{==-Set}}}}\, \,\htmlId{9632}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9589}{\htmlId{9633}{\htmlClass{Bound}{\text{m0}}}}\, \,\href{Axiom.Set.Map.html#2293}{\htmlId{9636}{\htmlClass{Function Operator}{\text{ˢ}}}}\,\,\htmlId{9637}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9639}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9604}{\htmlId{9640}{\htmlClass{Bound}{\text{m1}}}}\, \,\href{Axiom.Set.Map.html#2293}{\htmlId{9643}{\htmlClass{Function Operator}{\text{ˢ}}}}\,\,\htmlId{9644}{\htmlClass{Symbol}{\text{))}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{9647}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{9649}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9594}{\htmlId{9650}{\htmlClass{Bound}{\text{s0}}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9653}{\htmlClass{Function Operator}{\text{==}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9609}{\htmlId{9656}{\htmlClass{Bound}{\text{s1}}}}\,\,\htmlId{9658}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{9660}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{9662}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9599}{\htmlId{9663}{\htmlClass{Bound}{\text{q0}}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9666}{\htmlClass{Function Operator}{\text{==}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9614}{\htmlId{9669}{\htmlClass{Bound}{\text{q1}}}}\,\,\htmlId{9671}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9452}{\htmlId{9673}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{9690}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \,\htmlId{9706}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9708}{\htmlClass{Function Operator}{\text{\_==\_}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9452}{\htmlId{9713}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{9730}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \,\htmlId{9746}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9748}{\htmlClass{Function Operator}{\text{\_==\_}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9452}{\htmlId{9753}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{9770}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \,\htmlId{9784}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9786}{\htmlClass{Function Operator}{\text{\_==\_}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9452}{\htmlId{9791}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{9808}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9827}{\htmlId{9827}{\htmlClass{Bound}{\text{w0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9830}{\htmlId{9830}{\htmlClass{Bound}{\text{w1}}}}\, \,\htmlId{9833}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9297}{\htmlId{9835}{\htmlClass{Function}{\text{==-Set}}}}\, \,\htmlId{9842}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9827}{\htmlId{9843}{\htmlClass{Bound}{\text{w0}}}}\, \,\href{Axiom.Set.Map.html#2293}{\htmlId{9846}{\htmlClass{Function Operator}{\text{ˢ}}}}\,\,\htmlId{9847}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9849}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9830}{\htmlId{9850}{\htmlClass{Bound}{\text{w1}}}}\, \,\href{Axiom.Set.Map.html#2293}{\htmlId{9853}{\htmlClass{Function Operator}{\text{ˢ}}}}\,\,\htmlId{9854}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9452}{\htmlId{9856}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{9873}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \,\htmlId{9878}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{9880}{\htmlClass{Function Operator}{\text{\_==\_}}}}\, \,\htmlId{9886}{\htmlClass{Comment}{\text{-- See note "GovAction and GovProposal equality"}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9935}{\htmlId{9935}{\htmlClass{Function}{\text{==-GovAction}}}}\, \,\htmlId{9948}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1716}{\htmlId{9950}{\htmlClass{Record}{\text{GovAction}}}}\, \,\htmlId{9960}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1716}{\htmlId{9962}{\htmlClass{Record}{\text{GovAction}}}}\, \,\htmlId{9972}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{9974}{\htmlClass{Datatype}{\text{Bool}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9935}{\htmlId{9979}{\htmlClass{Function}{\text{==-GovAction}}}}\, \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9994}{\htmlId{9994}{\htmlClass{Bound}{\text{t0}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9999}{\htmlId{9999}{\htmlClass{Bound}{\text{d0}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10008}{\htmlId{10008}{\htmlClass{Bound}{\text{t1}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10013}{\htmlId{10013}{\htmlClass{Bound}{\text{d1}}}}\, \end{pmatrix} \,\htmlId{10024}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9994}{\htmlId{10029}{\htmlClass{Bound}{\text{t0}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10032}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10008}{\htmlId{10034}{\htmlClass{Bound}{\text{t1}}}}\, \,\htmlId{10037}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{10041}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{10043}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{10049}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{10054}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9452}{\htmlId{10056}{\htmlClass{Function}{\text{==-GovActionData}}}}\, \,\htmlId{10073}{\htmlClass{Bound}{\text{t1}}}\, \,\htmlId{10076}{\htmlClass{Bound}{\text{d0}}}\, \,\htmlId{10079}{\htmlClass{Bound}{\text{d1}}}\, \,\htmlId{10082}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{10086}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10088}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{10093}{\htmlClass{Symbol}{\text{\_}}}\, \,\htmlId{10095}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Bool.html#192}{\htmlId{10097}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10104}{\htmlId{10104}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10120}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{10122}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{10124}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10125}{\htmlId{10125}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{10126}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10128}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Class.DecEq.Core.html#126}{\htmlId{10130}{\htmlClass{Record}{\text{DecEq}}}}\, \,\htmlId{10136}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2894}{\htmlId{10137}{\htmlClass{Function}{\text{NeedsHash}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10125}{\htmlId{10147}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{10148}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10104}{\htmlId{10150}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10166}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{10167}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,\,\htmlId{10179}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10181}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10182}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10186}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10188}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10192}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2346}{\htmlId{10194}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{10203}{\htmlClass{Symbol}{\text{⦄}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10104}{\htmlId{10205}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10221}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{10222}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,\,\htmlId{10237}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10239}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10240}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10244}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10246}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10250}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2346}{\htmlId{10252}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{10261}{\htmlClass{Symbol}{\text{⦄}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10104}{\htmlId{10263}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10279}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{10280}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,\,\htmlId{10295}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10297}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10298}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10302}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10304}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10308}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2346}{\htmlId{10310}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{10319}{\htmlClass{Symbol}{\text{⦄}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10104}{\htmlId{10321}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10337}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{10338}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,\,\htmlId{10353}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10355}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10356}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10360}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10362}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10366}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2346}{\htmlId{10368}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{10377}{\htmlClass{Symbol}{\text{⦄}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10104}{\htmlId{10379}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10395}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{10396}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,\,\htmlId{10409}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10411}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10412}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10416}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10418}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10422}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2346}{\htmlId{10424}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{10433}{\htmlClass{Symbol}{\text{⦄}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10104}{\htmlId{10435}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10451}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{10452}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,\,\htmlId{10470}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10472}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10473}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10477}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10479}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10483}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Class.DecEq.Instances.html#193}{\htmlId{10485}{\htmlClass{Function}{\text{DecEq-⊤}}}}\, \,\htmlId{10493}{\htmlClass{Symbol}{\text{⦄}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10104}{\htmlId{10495}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{10511}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{10512}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,\,\htmlId{10516}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{10518}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10519}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10523}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10525}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{10529}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Class.DecEq.Instances.html#193}{\htmlId{10531}{\htmlClass{Function}{\text{DecEq-⊤}}}}\, \,\htmlId{10539}{\htmlClass{Symbol}{\text{⦄}}}\, \,\htmlId{10542}{\htmlClass{Comment}{\text{-- See note "GovAction and GovProposal equality"}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10591}{\htmlId{10591}{\htmlClass{Function}{\text{==-GovProposal}}}}\, \,\htmlId{10606}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3327}{\htmlId{10608}{\htmlClass{Record}{\text{GovProposal}}}}\, \,\htmlId{10620}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3327}{\htmlId{10622}{\htmlClass{Record}{\text{GovProposal}}}}\, \,\htmlId{10634}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{10636}{\htmlClass{Datatype}{\text{Bool}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10591}{\htmlId{10641}{\htmlClass{Function}{\text{==-GovProposal}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10656}{\htmlId{10656}{\htmlClass{Bound Operator}{\text{\_gp0}}}}\,\,\htmlId{10660}{\htmlClass{Symbol}{\text{@(}}}\,\,\htmlId{10662}{\htmlClass{InductiveConstructor}{\text{GovProposal.constructor}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10686}{\htmlId{10686}{\htmlClass{Bound}{\text{a0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10689}{\htmlId{10689}{\htmlClass{Bound}{\text{b0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10692}{\htmlId{10692}{\htmlClass{Bound}{\text{c0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10695}{\htmlId{10695}{\htmlClass{Bound}{\text{d0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10698}{\htmlId{10698}{\htmlClass{Bound}{\text{e0}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10701}{\htmlId{10701}{\htmlClass{Bound}{\text{f0}}}}\,\,\htmlId{10703}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10720}{\htmlId{10720}{\htmlClass{Bound Operator}{\text{\_gp1}}}}\,\,\htmlId{10724}{\htmlClass{Symbol}{\text{@(}}}\,\,\htmlId{10726}{\htmlClass{InductiveConstructor}{\text{GovProposal.constructor}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10750}{\htmlId{10750}{\htmlClass{Bound}{\text{a1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10753}{\htmlId{10753}{\htmlClass{Bound}{\text{b1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10756}{\htmlId{10756}{\htmlClass{Bound}{\text{c1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10759}{\htmlId{10759}{\htmlClass{Bound}{\text{d1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10762}{\htmlId{10762}{\htmlClass{Bound}{\text{e1}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10765}{\htmlId{10765}{\htmlClass{Bound}{\text{f1}}}}\,\,\htmlId{10767}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{10771}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1773}{\htmlId{10776}{\htmlClass{Field}{\text{GovAction.gaType}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10686}{\htmlId{10793}{\htmlClass{Bound}{\text{a0}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10796}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1773}{\htmlId{10798}{\htmlClass{Field}{\text{GovAction.gaType}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10750}{\htmlId{10815}{\htmlClass{Bound}{\text{a1}}}}\, \,\htmlId{10818}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{10822}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{10824}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{10830}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{10835}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#9935}{\htmlId{10841}{\htmlClass{Function}{\text{==-GovAction}}}}\, \,\htmlId{10854}{\htmlClass{Bound}{\text{a0}}}\, \,\htmlId{10857}{\htmlClass{Bound}{\text{a1}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{10864}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10866}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10867}{\htmlClass{Bound}{\text{b0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10870}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10873}{\htmlClass{Bound}{\text{b1}}}\,\,\htmlId{10875}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{10881}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10883}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10884}{\htmlClass{Bound}{\text{c0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10887}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10890}{\htmlClass{Bound}{\text{c1}}}\,\,\htmlId{10892}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{10898}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10900}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10901}{\htmlClass{Bound}{\text{d0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10904}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10907}{\htmlClass{Bound}{\text{d1}}}\,\,\htmlId{10909}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{10915}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10917}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10918}{\htmlClass{Bound}{\text{e0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10921}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10924}{\htmlClass{Bound}{\text{e1}}}\,\,\htmlId{10926}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.Bool.Base.html#1005}{\htmlId{10932}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{10934}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{10935}{\htmlClass{Bound}{\text{f0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{10938}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{10941}{\htmlClass{Bound}{\text{f1}}}\,\,\htmlId{10943}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{10947}{\htmlClass{Keyword}{\text{where}}}\, \,\htmlId{10957}{\htmlClass{Keyword}{\text{open}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#3327}{\htmlId{10962}{\htmlClass{Module}{\text{GovProposal}}}}\, \,\htmlId{10978}{\htmlClass{Keyword}{\text{instance}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10987}{\htmlId{10987}{\htmlClass{Function}{\text{\_}}}}\, \,\htmlId{10989}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#10104}{\htmlId{10991}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{11007}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{11011}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{11013}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{11018}{\htmlClass{Symbol}{\text{\_}}}\, \,\htmlId{11020}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Bool.html#192}{\htmlId{11022}{\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)