{-# OPTIONS --safe #-}
open import Ledger.Conway.Specification.Gov.Base
module Ledger.Conway.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)
data GovRole : Type where
CC DRep SPO : GovRole
instance
unquoteDecl Show-GovRole = derive-Show [ (quote GovRole , Show-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
record HasGovActionType (A : Type) : Type where
field GovActionTypeOf : A → GovActionType
open HasGovActionType ⦃...⦄ public
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
record HasGovAction (A : Type) : Type where
field GovActionOf : A → GovAction
open HasGovAction ⦃...⦄ 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
unquoteDecl DecEq-GovActionType = derive-DecEq ((quote GovActionType , DecEq-GovActionType) ∷ [])
==-Set : ∀ {A} ⦃ dA : DecEq A ⦄ → ℙ A → ℙ A → Bool
==-Set xs ys =
all (λ x → ⌊ x ∈? ys ⌋) (setToList xs) ∧
all (λ y → ⌊ y ∈? xs ⌋) (setToList ys)
==-GovActionData : ∀ A → GovActionData A → GovActionData A → Bool
==-GovActionData NoConfidence = _==_
==-GovActionData UpdateCommittee (m0 , s0 , q0) (m1 , s1 , q1) =
(==-Set (m0 ˢ) (m1 ˢ)) ∧ (s0 == s1) ∧ (q0 == q1)
==-GovActionData NewConstitution = _==_
==-GovActionData TriggerHardFork = _==_
==-GovActionData ChangePParams = _==_
==-GovActionData TreasuryWithdrawal w0 w1 = ==-Set (w0 ˢ) (w1 ˢ)
==-GovActionData Info = _==_
==-GovAction : GovAction → GovAction → Bool
==-GovAction $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2777}{\htmlId{2777}{\htmlClass{Bound}{\text{t0}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#2782}{\htmlId{2782}{\htmlClass{Bound}{\text{d0}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2791}{\htmlId{2791}{\htmlClass{Bound}{\text{t1}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#2796}{\htmlId{2796}{\htmlClass{Bound}{\text{d1}}}}\, \end{pmatrix}$
with t0 ≟ t1
... | P.yes refl = ==-GovActionData t1 d0 d1
... | P.no _ = false
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
field
url : String
hash : DocHash
record GovVote : Type where
field
gid : GovActionID
voter : GovVoter
vote : Vote
anchor : Maybe Anchor
record GovVotes : Type where
field
gvCC : Credential ⇀ Vote
gvDRep : Credential ⇀ Vote
gvSPO : KeyHash ⇀ Vote
data VDeleg : Type where
vDelegCredential : Credential → VDeleg
vDelegAbstain : VDeleg
vDelegNoConfidence : VDeleg
VoteDelegs : Type
VoteDelegs = Credential ⇀ VDeleg
record HasVoteDelegs {a} (A : Type a) : Type a where
field VoteDelegsOf : A → VoteDelegs
open HasVoteDelegs ⦃...⦄ public
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
instance
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₁
Policy : Type
Policy = Maybe ScriptHash
record GovProposal : Type where
field
action : GovAction
prevAction : NeedsHash (gaType action)
policy : Policy
deposit : Coin
returnAddr : RewardAddress
anchor : Anchor
record GovActionState : Type where
field
votes : GovVotes
returnAddr : RewardAddress
expiresIn : Epoch
action : GovAction
prevAction : NeedsHash (gaType action)
record HasGovVoter {a} (A : Type a) : Type a where
field GovVoterOf : A → GovVoter
open HasGovVoter ⦃...⦄ 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
instance
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
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
instance
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) ∷ [])
unquoteDecl DecEq-Anchor = derive-DecEq ((quote Anchor , DecEq-Anchor) ∷ [])
DecEq-GovVoter : DecEq GovVoter
DecEq-GovVoter ._≟_ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{6492}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#6499}{\htmlId{6499}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{6507}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#6514}{\htmlId{6514}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}$
with c ≟ c'
... | P.yes p = P.yes (cong $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{6569}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#6551}{\htmlId{6578}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{6579}{\htmlClass{Symbol}{\text{)}}}\,
\,\htmlId{6583}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6587}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6589}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6594}{\htmlId{6594}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{6597}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6599}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6604}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{6607}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6609}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{6614}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6594}{\htmlId{6616}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6619}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{6623}{\htmlClass{Symbol}{\text{})}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6436}{\htmlId{6628}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6643}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6644}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{6650}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#6657}{\htmlId{6657}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{6665}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#6672}{\htmlId{6672}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{6679}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6681}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6686}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{6688}{\htmlClass{Symbol}{\text{()}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6436}{\htmlId{6693}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6708}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6709}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{6715}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6722}{\htmlId{6722}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{6730}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6737}{\htmlId{6737}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{6744}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6746}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6751}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{6753}{\htmlClass{Symbol}{\text{()}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6436}{\htmlId{6758}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6773}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6774}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{6780}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6787}{\htmlId{6787}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{6795}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6802}{\htmlId{6802}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{6809}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6811}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6816}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{6818}{\htmlClass{Symbol}{\text{()}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6436}{\htmlId{6823}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6838}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6839}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{6845}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6852}{\htmlId{6852}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{6860}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6867}{\htmlId{6867}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
\,\htmlId{6878}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6852}{\htmlId{6883}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{6885}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6867}{\htmlId{6887}{\htmlClass{Bound}{\text{c'}}}}\,
\,\htmlId{6892}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6896}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{6898}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6904}{\htmlId{6904}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{6906}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{6908}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{6914}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{6915}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{6922}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6904}{\htmlId{6933}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{6934}{\htmlClass{Symbol}{\text{)}}}\,
\,\htmlId{6938}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6942}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6944}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6949}{\htmlId{6949}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{6952}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6954}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6959}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{6962}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6964}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{6969}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6949}{\htmlId{6971}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6974}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{6978}{\htmlClass{Symbol}{\text{})}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6436}{\htmlId{6983}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6998}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6999}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{7005}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7012}{\htmlId{7012}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{7020}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7027}{\htmlId{7027}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{7034}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7036}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7041}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{7043}{\htmlClass{Symbol}{\text{()}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6436}{\htmlId{7048}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7063}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7064}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{7070}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7077}{\htmlId{7077}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{7085}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7092}{\htmlId{7092}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{7099}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7101}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7106}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{7108}{\htmlClass{Symbol}{\text{()}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6436}{\htmlId{7113}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7128}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7129}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{7135}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7142}{\htmlId{7142}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{7150}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7157}{\htmlId{7157}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{7164}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7166}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7171}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{7173}{\htmlClass{Symbol}{\text{()}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6436}{\htmlId{7178}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7193}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7194}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{7200}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7207}{\htmlId{7207}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{7215}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7222}{\htmlId{7222}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
\,\htmlId{7233}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7207}{\htmlId{7238}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7240}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7222}{\htmlId{7242}{\htmlClass{Bound}{\text{c'}}}}\,
\,\htmlId{7247}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{7251}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{7253}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7259}{\htmlId{7259}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{7261}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{7263}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{7269}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{7270}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{7277}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7259}{\htmlId{7287}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{7288}{\htmlClass{Symbol}{\text{)}}}\,
\,\htmlId{7292}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{7296}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7298}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7303}{\htmlId{7303}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{7306}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7308}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7313}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{7316}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{7318}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{7323}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7303}{\htmlId{7325}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{7328}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{7332}{\htmlClass{Symbol}{\text{})}}}\,
\,\htmlId{7338}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7350}{\htmlId{7350}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{7366}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{7368}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{7383}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{7385}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{7386}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#3202}{\htmlId{7392}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7350}{\htmlId{7402}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{7417}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{7419}{\htmlClass{Function Operator}{\text{]}}}}\,
\,\htmlId{7424}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7436}{\htmlId{7436}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{7448}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{7450}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{7462}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{7464}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{7465}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#3478}{\htmlId{7471}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7436}{\htmlId{7480}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{7491}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{7493}{\htmlClass{Function Operator}{\text{]}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7496}{\htmlId{7496}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7512}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{7514}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{7516}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#7517}{\htmlId{7517}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{7518}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7520}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Class.DecEq.Core.html#126}{\htmlId{7522}{\htmlClass{Record}{\text{DecEq}}}}\, \,\htmlId{7528}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#3782}{\htmlId{7529}{\htmlClass{Function}{\text{NeedsHash}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7517}{\htmlId{7539}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{7540}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7496}{\htmlId{7542}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7558}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#656}{\htmlId{7559}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,\,\htmlId{7571}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7573}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7574}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7578}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7580}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7584}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{7586}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{7595}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7496}{\htmlId{7597}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7613}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#694}{\htmlId{7614}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,\,\htmlId{7629}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7631}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7632}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7636}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7638}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7642}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{7644}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{7653}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7496}{\htmlId{7655}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7671}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#732}{\htmlId{7672}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,\,\htmlId{7687}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7689}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7690}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7694}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7696}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7700}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{7702}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{7711}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7496}{\htmlId{7713}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7729}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#770}{\htmlId{7730}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,\,\htmlId{7745}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7747}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7748}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7752}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7754}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7758}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{7760}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{7769}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7496}{\htmlId{7771}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7787}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#808}{\htmlId{7788}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,\,\htmlId{7801}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7803}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7804}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7808}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7810}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7814}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{7816}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{7825}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7496}{\htmlId{7827}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7843}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#846}{\htmlId{7844}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,\,\htmlId{7862}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7864}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7865}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7869}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7871}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7875}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Class.DecEq.Instances.html#193}{\htmlId{7877}{\htmlClass{Function}{\text{DecEq-⊤}}}}\, \,\htmlId{7885}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7496}{\htmlId{7887}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7903}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#884}{\htmlId{7904}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,\,\htmlId{7908}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7910}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7911}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7915}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7917}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7921}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Class.DecEq.Instances.html#193}{\htmlId{7923}{\htmlClass{Function}{\text{DecEq-⊤}}}}\, \,\htmlId{7931}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\htmlId{7934}{\htmlClass{Comment}{\text{-- See note "GovAction and GovProposal equality"}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7983}{\htmlId{7983}{\htmlClass{Function}{\text{==-GovProposal}}}}\, \,\htmlId{7998}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#4511}{\htmlId{8000}{\htmlClass{Record}{\text{GovProposal}}}}\, \,\htmlId{8012}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#4511}{\htmlId{8014}{\htmlClass{Record}{\text{GovProposal}}}}\, \,\htmlId{8026}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{8028}{\htmlClass{Datatype}{\text{Bool}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7983}{\htmlId{8033}{\htmlClass{Function}{\text{==-GovProposal}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8048}{\htmlId{8048}{\htmlClass{Bound Operator}{\text{\_gp0}}}}\,\,\htmlId{8052}{\htmlClass{Symbol}{\text{@(}}}\,\,\htmlId{8054}{\htmlClass{InductiveConstructor}{\text{GovProposal.constructor}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8078}{\htmlId{8078}{\htmlClass{Bound}{\text{a0}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8081}{\htmlId{8081}{\htmlClass{Bound}{\text{b0}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8084}{\htmlId{8084}{\htmlClass{Bound}{\text{c0}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8087}{\htmlId{8087}{\htmlClass{Bound}{\text{d0}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8090}{\htmlId{8090}{\htmlClass{Bound}{\text{e0}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8093}{\htmlId{8093}{\htmlClass{Bound}{\text{f0}}}}\,\,\htmlId{8095}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8112}{\htmlId{8112}{\htmlClass{Bound Operator}{\text{\_gp1}}}}\,\,\htmlId{8116}{\htmlClass{Symbol}{\text{@(}}}\,\,\htmlId{8118}{\htmlClass{InductiveConstructor}{\text{GovProposal.constructor}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8142}{\htmlId{8142}{\htmlClass{Bound}{\text{a1}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8145}{\htmlId{8145}{\htmlClass{Bound}{\text{b1}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8148}{\htmlId{8148}{\htmlClass{Bound}{\text{c1}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8151}{\htmlId{8151}{\htmlClass{Bound}{\text{d1}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8154}{\htmlId{8154}{\htmlClass{Bound}{\text{e1}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8157}{\htmlId{8157}{\htmlClass{Bound}{\text{f1}}}}\,\,\htmlId{8159}{\htmlClass{Symbol}{\text{)}}}\,
\,\htmlId{8163}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#1515}{\htmlId{8168}{\htmlClass{Field}{\text{GovAction.gaType}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8078}{\htmlId{8185}{\htmlClass{Bound}{\text{a0}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8188}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#1515}{\htmlId{8190}{\htmlClass{Field}{\text{GovAction.gaType}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8142}{\htmlId{8207}{\htmlClass{Bound}{\text{a1}}}}\,
\,\htmlId{8210}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8214}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8216}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8222}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8227}{\htmlClass{Symbol}{\text{=}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#2718}{\htmlId{8233}{\htmlClass{Function}{\text{==-GovAction}}}}\, \,\htmlId{8246}{\htmlClass{Bound}{\text{a0}}}\, \,\htmlId{8249}{\htmlClass{Bound}{\text{a1}}}\,
\,\href{Data.Bool.Base.html#1005}{\htmlId{8256}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{8258}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8259}{\htmlClass{Bound}{\text{b0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{8262}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{8265}{\htmlClass{Bound}{\text{b1}}}\,\,\htmlId{8267}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Data.Bool.Base.html#1005}{\htmlId{8273}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{8275}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8276}{\htmlClass{Bound}{\text{c0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{8279}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{8282}{\htmlClass{Bound}{\text{c1}}}\,\,\htmlId{8284}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Data.Bool.Base.html#1005}{\htmlId{8290}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{8292}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8293}{\htmlClass{Bound}{\text{d0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{8296}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{8299}{\htmlClass{Bound}{\text{d1}}}\,\,\htmlId{8301}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Data.Bool.Base.html#1005}{\htmlId{8307}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{8309}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8310}{\htmlClass{Bound}{\text{e0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{8313}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{8316}{\htmlClass{Bound}{\text{e1}}}\,\,\htmlId{8318}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Data.Bool.Base.html#1005}{\htmlId{8324}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{8326}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8327}{\htmlClass{Bound}{\text{f0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{8330}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{8333}{\htmlClass{Bound}{\text{f1}}}\,\,\htmlId{8335}{\htmlClass{Symbol}{\text{)}}}\,
\,\htmlId{8339}{\htmlClass{Keyword}{\text{where}}}\,
\,\htmlId{8349}{\htmlClass{Keyword}{\text{open}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#4511}{\htmlId{8354}{\htmlClass{Module}{\text{GovProposal}}}}\,
\,\htmlId{8370}{\htmlClass{Keyword}{\text{instance}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8379}{\htmlId{8379}{\htmlClass{Function}{\text{\_}}}}\, \,\htmlId{8381}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7496}{\htmlId{8383}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\,
\,\htmlId{8399}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8403}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8405}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8410}{\htmlClass{Symbol}{\text{\_}}}\, \,\htmlId{8412}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Bool.html#192}{\htmlId{8414}{\htmlClass{InductiveConstructor}{\text{false}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8422}{\htmlId{8422}{\htmlClass{Function}{\text{isGovVoterDRep}}}}\, \,\htmlId{8437}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#2990}{\htmlId{8439}{\htmlClass{Record}{\text{GovVoter}}}}\, \,\htmlId{8448}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Maybe.html#135}{\htmlId{8450}{\htmlClass{Datatype}{\text{Maybe}}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{8456}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8422}{\htmlId{8467}{\htmlClass{Function}{\text{isGovVoterDRep}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{8484}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#8491}{\htmlId{8491}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{8497}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{8499}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8491}{\htmlId{8504}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8422}{\htmlId{8506}{\htmlClass{CatchallClause Function}{\text{isGovVoterDRep}}}}\,\,\htmlId{8520}{\htmlClass{CatchallClause}{\text{ }}}\,\,\htmlId{8521}{\htmlClass{CatchallClause Symbol}{\text{\_}}}\, \,\htmlId{8523}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{8525}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8534}{\htmlId{8534}{\htmlClass{Function}{\text{govVoterCredential}}}}\, \,\htmlId{8553}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#2990}{\htmlId{8555}{\htmlClass{Record}{\text{GovVoter}}}}\, \,\htmlId{8564}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{8566}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8534}{\htmlId{8577}{\htmlClass{Function}{\text{govVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{8598}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#8605}{\htmlId{8605}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{8612}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8605}{\htmlId{8614}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8534}{\htmlId{8616}{\htmlClass{Function}{\text{govVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{8637}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#8644}{\htmlId{8644}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{8651}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8644}{\htmlId{8653}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8534}{\htmlId{8655}{\htmlClass{Function}{\text{govVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{8676}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#8683}{\htmlId{8683}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix} \,\htmlId{8690}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Core.Specification.Address.html#285}{\htmlId{8692}{\htmlClass{InductiveConstructor}{\text{KeyHashObj}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8683}{\htmlId{8703}{\htmlClass{Bound}{\text{kh}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8707}{\htmlId{8707}{\htmlClass{Function}{\text{proposedCC}}}}\, \,\htmlId{8718}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#1454}{\htmlId{8720}{\htmlClass{Record}{\text{GovAction}}}}\, \,\htmlId{8730}{\htmlClass{Symbol}{\text{→}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#488}{\htmlId{8732}{\htmlClass{Function Operator}{\text{ℙ}}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{8734}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8707}{\htmlId{8745}{\htmlClass{Function}{\text{proposedCC}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#694}{\htmlId{8758}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, , \,\htmlId{8776}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#8777}{\htmlId{8777}{\htmlClass{Bound}{\text{x}}}}\, , \,\htmlId{8781}{\htmlClass{Symbol}{\text{\_}}}\, , \,\htmlId{8785}{\htmlClass{Symbol}{\text{\_)}}}\, \end{pmatrix} \,\htmlId{8792}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.IsSet.html#916}{\htmlId{8794}{\htmlClass{Function}{\text{dom}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8777}{\htmlId{8798}{\htmlClass{Bound}{\text{x}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8707}{\htmlId{8800}{\htmlClass{CatchallClause Function}{\text{proposedCC}}}}\,\,\htmlId{8810}{\htmlClass{CatchallClause}{\text{ }}}\,\,\htmlId{8811}{\htmlClass{CatchallClause Symbol}{\text{\_}}}\, \,\htmlId{8813}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.HasEmptySet.html#287}{\htmlId{8815}{\htmlClass{Field}{\text{∅}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8819}{\htmlId{8819}{\htmlClass{Function}{\text{DReps}}}}\, \,\htmlId{8825}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{8827}{\htmlClass{Primitive}{\text{Type}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8819}{\htmlId{8832}{\htmlClass{Function}{\text{DReps}}}}\, \,\htmlId{8838}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{8840}{\htmlClass{Datatype}{\text{Credential}}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#633}{\htmlId{8851}{\htmlClass{Function Operator}{\text{⇀}}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{8853}{\htmlClass{Function}{\text{Epoch}}}}\,
\,\htmlId{8861}{\htmlClass{Keyword}{\text{record}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8868}{\htmlId{8868}{\htmlClass{Record}{\text{HasDReps}}}}\, \,\htmlId{8877}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#8878}{\htmlId{8878}{\htmlClass{Bound}{\text{a}}}}\,\,\htmlId{8879}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{8881}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#8882}{\htmlId{8882}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8884}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{8886}{\htmlClass{Primitive}{\text{Type}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8878}{\htmlId{8891}{\htmlClass{Bound}{\text{a}}}}\,\,\htmlId{8892}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{8894}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{8896}{\htmlClass{Primitive}{\text{Type}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8878}{\htmlId{8901}{\htmlClass{Bound}{\text{a}}}}\, \,\htmlId{8903}{\htmlClass{Keyword}{\text{where}}}\,
\,\htmlId{8911}{\htmlClass{Keyword}{\text{field}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8917}{\htmlId{8917}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\htmlId{8925}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8882}{\htmlId{8927}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8929}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8819}{\htmlId{8931}{\htmlClass{Function}{\text{DReps}}}}\,
\,\htmlId{8937}{\htmlClass{Keyword}{\text{open}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8868}{\htmlId{8942}{\htmlClass{Module}{\text{HasDReps}}}}\, \,\htmlId{8951}{\htmlClass{Symbol}{\text{⦃...⦄}}}\, \,\htmlId{8957}{\htmlClass{Keyword}{\text{public}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8966}{\htmlId{8966}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\htmlId{8980}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{8982}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{8988}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{8990}{\htmlClass{Datatype}{\text{Credential}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{9001}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{9003}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{9009}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{9011}{\htmlClass{Primitive}{\text{Type}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8966}{\htmlId{9016}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9030}{\htmlId{9030}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{9032}{\htmlClass{Symbol}{\text{(\_}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#9037}{\htmlId{9037}{\htmlClass{Bound}{\text{expEpoch}}}}\,\,\htmlId{9045}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9047}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9030}{\htmlId{9049}{\htmlClass{Bound}{\text{e}}}}\, \,\href{Class.HasOrder.Core.html#613}{\htmlId{9051}{\htmlClass{Field Operator}{\text{≤}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9037}{\htmlId{9053}{\htmlClass{Bound}{\text{expEpoch}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#9063}{\htmlId{9063}{\htmlClass{Function}{\text{activeDRepsOf}}}}\, \,\htmlId{9077}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{9079}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#9080}{\htmlId{9080}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9082}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{9084}{\htmlClass{Primitive}{\text{Type}}}}\,\,\htmlId{9088}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{9090}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9092}{\htmlId{9092}{\htmlClass{Bound}{\text{\_}}}}\, \,\htmlId{9094}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8868}{\htmlId{9096}{\htmlClass{Record}{\text{HasDReps}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9080}{\htmlId{9105}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9107}{\htmlClass{Symbol}{\text{⦄}}}\, \,\htmlId{9109}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9080}{\htmlId{9111}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9113}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{9115}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{9121}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8819}{\htmlId{9123}{\htmlClass{Function}{\text{DReps}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#9063}{\htmlId{9129}{\htmlClass{Function}{\text{activeDRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9143}{\htmlId{9143}{\htmlClass{Bound}{\text{a}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9145}{\htmlId{9145}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{9147}{\htmlClass{Symbol}{\text{=}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#4102}{\htmlId{9149}{\htmlClass{Function}{\text{filterᵐ}}}}\, \,\htmlId{9157}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#8966}{\htmlId{9158}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9145}{\htmlId{9172}{\htmlClass{Bound}{\text{e}}}}\,\,\htmlId{9173}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9175}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#8917}{\htmlId{9176}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9143}{\htmlId{9184}{\htmlClass{Bound}{\text{a}}}}\,\,\htmlId{9185}{\htmlClass{Symbol}{\text{)}}}\,