{-# 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)
open import Ledger.Core.Specification.ProtocolVersion
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#2831}{\htmlId{2831}{\htmlClass{Bound}{\text{t0}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#2836}{\htmlId{2836}{\htmlClass{Bound}{\text{d0}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2845}{\htmlId{2845}{\htmlClass{Bound}{\text{t1}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#2850}{\htmlId{2850}{\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#423}{\htmlId{6546}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#6553}{\htmlId{6553}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#423}{\htmlId{6561}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#6568}{\htmlId{6568}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}$
with c ≟ c'
... | P.yes p = P.yes (cong $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#423}{\htmlId{6623}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#6605}{\htmlId{6632}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{6633}{\htmlClass{Symbol}{\text{)}}}\,
\,\htmlId{6637}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6641}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6643}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6648}{\htmlId{6648}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{6651}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6653}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6658}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{6661}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6663}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{6668}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6648}{\htmlId{6670}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6673}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{6677}{\htmlClass{Symbol}{\text{})}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6490}{\htmlId{6682}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6697}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6698}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#423}{\htmlId{6704}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#6711}{\htmlId{6711}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#426}{\htmlId{6719}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#6726}{\htmlId{6726}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{6733}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6735}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6740}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{6742}{\htmlClass{Symbol}{\text{()}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6490}{\htmlId{6747}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6762}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6763}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#423}{\htmlId{6769}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6776}{\htmlId{6776}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#431}{\htmlId{6784}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6791}{\htmlId{6791}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{6798}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6800}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6805}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{6807}{\htmlClass{Symbol}{\text{()}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6490}{\htmlId{6812}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6827}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6828}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#426}{\htmlId{6834}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6841}{\htmlId{6841}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#423}{\htmlId{6849}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6856}{\htmlId{6856}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{6863}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6865}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6870}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{6872}{\htmlClass{Symbol}{\text{()}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6490}{\htmlId{6877}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6892}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6893}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#426}{\htmlId{6899}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6906}{\htmlId{6906}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#426}{\htmlId{6914}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6921}{\htmlId{6921}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
\,\htmlId{6932}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6906}{\htmlId{6937}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{6939}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6921}{\htmlId{6941}{\htmlClass{Bound}{\text{c'}}}}\,
\,\htmlId{6946}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6950}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{6952}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6958}{\htmlId{6958}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{6960}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{6962}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{6968}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{6969}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#426}{\htmlId{6976}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6958}{\htmlId{6987}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{6988}{\htmlClass{Symbol}{\text{)}}}\,
\,\htmlId{6992}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6996}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6998}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7003}{\htmlId{7003}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{7006}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7008}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7013}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{7016}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{7018}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{7023}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7003}{\htmlId{7025}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{7028}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{7032}{\htmlClass{Symbol}{\text{})}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6490}{\htmlId{7037}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7052}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7053}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#426}{\htmlId{7059}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7066}{\htmlId{7066}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#431}{\htmlId{7074}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7081}{\htmlId{7081}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{7088}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7090}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7095}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{7097}{\htmlClass{Symbol}{\text{()}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6490}{\htmlId{7102}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7117}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7118}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#431}{\htmlId{7124}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7131}{\htmlId{7131}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#423}{\htmlId{7139}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7146}{\htmlId{7146}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{7153}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7155}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7160}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{7162}{\htmlClass{Symbol}{\text{()}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6490}{\htmlId{7167}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7182}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7183}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#431}{\htmlId{7189}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7196}{\htmlId{7196}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#426}{\htmlId{7204}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7211}{\htmlId{7211}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{7218}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7220}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7225}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{7227}{\htmlClass{Symbol}{\text{()}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6490}{\htmlId{7232}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{7247}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7248}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#431}{\htmlId{7254}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7261}{\htmlId{7261}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#431}{\htmlId{7269}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7276}{\htmlId{7276}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
\,\htmlId{7287}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7261}{\htmlId{7292}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7294}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7276}{\htmlId{7296}{\htmlClass{Bound}{\text{c'}}}}\,
\,\htmlId{7301}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{7305}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{7307}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7313}{\htmlId{7313}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{7315}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{7317}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{7323}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{7324}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#431}{\htmlId{7331}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7313}{\htmlId{7341}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{7342}{\htmlClass{Symbol}{\text{)}}}\,
\,\htmlId{7346}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{7350}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7352}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7357}{\htmlId{7357}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{7360}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{7362}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{7367}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{7370}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{7372}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{7377}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7357}{\htmlId{7379}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{7382}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{7386}{\htmlClass{Symbol}{\text{})}}}\,
\,\htmlId{7392}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7404}{\htmlId{7404}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{7420}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{7422}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{7437}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{7439}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{7440}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#3256}{\htmlId{7446}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7404}{\htmlId{7456}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{7471}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{7473}{\htmlClass{Function Operator}{\text{]}}}}\,
\,\htmlId{7478}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7490}{\htmlId{7490}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{7502}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{7504}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{7516}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{7518}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{7519}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#3532}{\htmlId{7525}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7490}{\htmlId{7534}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{7545}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{7547}{\htmlClass{Function Operator}{\text{]}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7550}{\htmlId{7550}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7566}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{7568}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{7570}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#7571}{\htmlId{7571}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{7572}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7574}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Class.DecEq.Core.html#126}{\htmlId{7576}{\htmlClass{Record}{\text{DecEq}}}}\, \,\htmlId{7582}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#3836}{\htmlId{7583}{\htmlClass{Function}{\text{NeedsHash}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7571}{\htmlId{7593}{\htmlClass{Bound}{\text{A}}}}\,\,\htmlId{7594}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7550}{\htmlId{7596}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7612}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#710}{\htmlId{7613}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,\,\htmlId{7625}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7627}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7628}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7632}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7634}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7638}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{7640}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{7649}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7550}{\htmlId{7651}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7667}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#748}{\htmlId{7668}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,\,\htmlId{7683}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7685}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7686}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7690}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7692}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7696}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{7698}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{7707}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7550}{\htmlId{7709}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7725}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#786}{\htmlId{7726}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,\,\htmlId{7741}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7743}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7744}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7748}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7750}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7754}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{7756}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{7765}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7550}{\htmlId{7767}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7783}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#824}{\htmlId{7784}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,\,\htmlId{7799}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7801}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7802}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7806}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7808}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7812}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{7814}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{7823}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7550}{\htmlId{7825}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7841}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#862}{\htmlId{7842}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,\,\htmlId{7855}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7857}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7858}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7862}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7864}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7868}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Prelude.html#2274}{\htmlId{7870}{\htmlClass{Function}{\text{DecEq-×′}}}}\, \,\htmlId{7879}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7550}{\htmlId{7881}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7897}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#900}{\htmlId{7898}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,\,\htmlId{7916}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7918}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7919}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7923}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7925}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7929}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Class.DecEq.Instances.html#193}{\htmlId{7931}{\htmlClass{Function}{\text{DecEq-⊤}}}}\, \,\htmlId{7939}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7550}{\htmlId{7941}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\, \,\htmlId{7957}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#938}{\htmlId{7958}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,\,\htmlId{7962}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7964}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{7965}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7969}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{7971}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \,\htmlId{7975}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Class.DecEq.Instances.html#193}{\htmlId{7977}{\htmlClass{Function}{\text{DecEq-⊤}}}}\, \,\htmlId{7985}{\htmlClass{Symbol}{\text{⦄}}}\,
\,\htmlId{7988}{\htmlClass{Comment}{\text{-- See note "GovAction and GovProposal equality"}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8037}{\htmlId{8037}{\htmlClass{Function}{\text{==-GovProposal}}}}\, \,\htmlId{8052}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#4565}{\htmlId{8054}{\htmlClass{Record}{\text{GovProposal}}}}\, \,\htmlId{8066}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#4565}{\htmlId{8068}{\htmlClass{Record}{\text{GovProposal}}}}\, \,\htmlId{8080}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Bool.html#173}{\htmlId{8082}{\htmlClass{Datatype}{\text{Bool}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8037}{\htmlId{8087}{\htmlClass{Function}{\text{==-GovProposal}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8102}{\htmlId{8102}{\htmlClass{Bound Operator}{\text{\_gp0}}}}\,\,\htmlId{8106}{\htmlClass{Symbol}{\text{@(}}}\,\,\htmlId{8108}{\htmlClass{InductiveConstructor}{\text{GovProposal.constructor}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8132}{\htmlId{8132}{\htmlClass{Bound}{\text{a0}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8135}{\htmlId{8135}{\htmlClass{Bound}{\text{b0}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8138}{\htmlId{8138}{\htmlClass{Bound}{\text{c0}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8141}{\htmlId{8141}{\htmlClass{Bound}{\text{d0}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8144}{\htmlId{8144}{\htmlClass{Bound}{\text{e0}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8147}{\htmlId{8147}{\htmlClass{Bound}{\text{f0}}}}\,\,\htmlId{8149}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8166}{\htmlId{8166}{\htmlClass{Bound Operator}{\text{\_gp1}}}}\,\,\htmlId{8170}{\htmlClass{Symbol}{\text{@(}}}\,\,\htmlId{8172}{\htmlClass{InductiveConstructor}{\text{GovProposal.constructor}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8196}{\htmlId{8196}{\htmlClass{Bound}{\text{a1}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8199}{\htmlId{8199}{\htmlClass{Bound}{\text{b1}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8202}{\htmlId{8202}{\htmlClass{Bound}{\text{c1}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8205}{\htmlId{8205}{\htmlClass{Bound}{\text{d1}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8208}{\htmlId{8208}{\htmlClass{Bound}{\text{e1}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8211}{\htmlId{8211}{\htmlClass{Bound}{\text{f1}}}}\,\,\htmlId{8213}{\htmlClass{Symbol}{\text{)}}}\,
\,\htmlId{8217}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#1569}{\htmlId{8222}{\htmlClass{Field}{\text{GovAction.gaType}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8132}{\htmlId{8239}{\htmlClass{Bound}{\text{a0}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{8242}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#1569}{\htmlId{8244}{\htmlClass{Field}{\text{GovAction.gaType}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8196}{\htmlId{8261}{\htmlClass{Bound}{\text{a1}}}}\,
\,\htmlId{8264}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8268}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{8270}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{8276}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{8281}{\htmlClass{Symbol}{\text{=}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#2772}{\htmlId{8287}{\htmlClass{Function}{\text{==-GovAction}}}}\, \,\htmlId{8300}{\htmlClass{Bound}{\text{a0}}}\, \,\htmlId{8303}{\htmlClass{Bound}{\text{a1}}}\,
\,\href{Data.Bool.Base.html#1005}{\htmlId{8310}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{8312}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8313}{\htmlClass{Bound}{\text{b0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{8316}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{8319}{\htmlClass{Bound}{\text{b1}}}\,\,\htmlId{8321}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Data.Bool.Base.html#1005}{\htmlId{8327}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{8329}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8330}{\htmlClass{Bound}{\text{c0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{8333}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{8336}{\htmlClass{Bound}{\text{c1}}}\,\,\htmlId{8338}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Data.Bool.Base.html#1005}{\htmlId{8344}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{8346}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8347}{\htmlClass{Bound}{\text{d0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{8350}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{8353}{\htmlClass{Bound}{\text{d1}}}\,\,\htmlId{8355}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Data.Bool.Base.html#1005}{\htmlId{8361}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{8363}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8364}{\htmlClass{Bound}{\text{e0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{8367}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{8370}{\htmlClass{Bound}{\text{e1}}}\,\,\htmlId{8372}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Data.Bool.Base.html#1005}{\htmlId{8378}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{8380}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{8381}{\htmlClass{Bound}{\text{f0}}}\, \,\href{Class.DecEq.Core.html#197}{\htmlId{8384}{\htmlClass{Function Operator}{\text{==}}}}\, \,\htmlId{8387}{\htmlClass{Bound}{\text{f1}}}\,\,\htmlId{8389}{\htmlClass{Symbol}{\text{)}}}\,
\,\htmlId{8393}{\htmlClass{Keyword}{\text{where}}}\,
\,\htmlId{8403}{\htmlClass{Keyword}{\text{open}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#4565}{\htmlId{8408}{\htmlClass{Module}{\text{GovProposal}}}}\,
\,\htmlId{8424}{\htmlClass{Keyword}{\text{instance}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8433}{\htmlId{8433}{\htmlClass{Function}{\text{\_}}}}\, \,\htmlId{8435}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7550}{\htmlId{8437}{\htmlClass{Function}{\text{DecEq-NeedsHash}}}}\,
\,\htmlId{8453}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{8457}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{8459}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{8464}{\htmlClass{Symbol}{\text{\_}}}\, \,\htmlId{8466}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Bool.html#192}{\htmlId{8468}{\htmlClass{InductiveConstructor}{\text{false}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8476}{\htmlId{8476}{\htmlClass{Function}{\text{isGovVoterDRep}}}}\, \,\htmlId{8491}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#3044}{\htmlId{8493}{\htmlClass{Record}{\text{GovVoter}}}}\, \,\htmlId{8502}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Maybe.html#135}{\htmlId{8504}{\htmlClass{Datatype}{\text{Maybe}}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{8510}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8476}{\htmlId{8521}{\htmlClass{Function}{\text{isGovVoterDRep}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#426}{\htmlId{8538}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#8545}{\htmlId{8545}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{8551}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{8553}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8545}{\htmlId{8558}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8476}{\htmlId{8560}{\htmlClass{CatchallClause Function}{\text{isGovVoterDRep}}}}\,\,\htmlId{8574}{\htmlClass{CatchallClause}{\text{ }}}\,\,\htmlId{8575}{\htmlClass{CatchallClause Symbol}{\text{\_}}}\, \,\htmlId{8577}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{8579}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8588}{\htmlId{8588}{\htmlClass{Function}{\text{govVoterCredential}}}}\, \,\htmlId{8607}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#3044}{\htmlId{8609}{\htmlClass{Record}{\text{GovVoter}}}}\, \,\htmlId{8618}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{8620}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8588}{\htmlId{8631}{\htmlClass{Function}{\text{govVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#423}{\htmlId{8652}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#8659}{\htmlId{8659}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{8666}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8659}{\htmlId{8668}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8588}{\htmlId{8670}{\htmlClass{Function}{\text{govVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#426}{\htmlId{8691}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#8698}{\htmlId{8698}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{8705}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8698}{\htmlId{8707}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8588}{\htmlId{8709}{\htmlClass{Function}{\text{govVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#431}{\htmlId{8730}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#8737}{\htmlId{8737}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix} \,\htmlId{8744}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Core.Specification.Address.html#285}{\htmlId{8746}{\htmlClass{InductiveConstructor}{\text{KeyHashObj}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8737}{\htmlId{8757}{\htmlClass{Bound}{\text{kh}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8761}{\htmlId{8761}{\htmlClass{Function}{\text{proposedCC}}}}\, \,\htmlId{8772}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#1508}{\htmlId{8774}{\htmlClass{Record}{\text{GovAction}}}}\, \,\htmlId{8784}{\htmlClass{Symbol}{\text{→}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#488}{\htmlId{8786}{\htmlClass{Function Operator}{\text{ℙ}}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{8788}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8761}{\htmlId{8799}{\htmlClass{Function}{\text{proposedCC}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#748}{\htmlId{8812}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, , \,\htmlId{8830}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#8831}{\htmlId{8831}{\htmlClass{Bound}{\text{x}}}}\, , \,\htmlId{8835}{\htmlClass{Symbol}{\text{\_}}}\, , \,\htmlId{8839}{\htmlClass{Symbol}{\text{\_)}}}\, \end{pmatrix} \,\htmlId{8846}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.IsSet.html#916}{\htmlId{8848}{\htmlClass{Function}{\text{dom}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8831}{\htmlId{8852}{\htmlClass{Bound}{\text{x}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8761}{\htmlId{8854}{\htmlClass{CatchallClause Function}{\text{proposedCC}}}}\,\,\htmlId{8864}{\htmlClass{CatchallClause}{\text{ }}}\,\,\htmlId{8865}{\htmlClass{CatchallClause Symbol}{\text{\_}}}\, \,\htmlId{8867}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.HasEmptySet.html#287}{\htmlId{8869}{\htmlClass{Field}{\text{∅}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8873}{\htmlId{8873}{\htmlClass{Function}{\text{DReps}}}}\, \,\htmlId{8879}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{8881}{\htmlClass{Primitive}{\text{Type}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#8873}{\htmlId{8886}{\htmlClass{Function}{\text{DReps}}}}\, \,\htmlId{8892}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{8894}{\htmlClass{Datatype}{\text{Credential}}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#633}{\htmlId{8905}{\htmlClass{Function Operator}{\text{⇀}}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{8907}{\htmlClass{Function}{\text{Epoch}}}}\,
\,\htmlId{8915}{\htmlClass{Keyword}{\text{record}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8922}{\htmlId{8922}{\htmlClass{Record}{\text{HasDReps}}}}\, \,\htmlId{8931}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#8932}{\htmlId{8932}{\htmlClass{Bound}{\text{a}}}}\,\,\htmlId{8933}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{8935}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#8936}{\htmlId{8936}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8938}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{8940}{\htmlClass{Primitive}{\text{Type}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8932}{\htmlId{8945}{\htmlClass{Bound}{\text{a}}}}\,\,\htmlId{8946}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{8948}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{8950}{\htmlClass{Primitive}{\text{Type}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8932}{\htmlId{8955}{\htmlClass{Bound}{\text{a}}}}\, \,\htmlId{8957}{\htmlClass{Keyword}{\text{where}}}\,
\,\htmlId{8965}{\htmlClass{Keyword}{\text{field}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8971}{\htmlId{8971}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\htmlId{8979}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8936}{\htmlId{8981}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{8983}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8873}{\htmlId{8985}{\htmlClass{Function}{\text{DReps}}}}\,
\,\htmlId{8991}{\htmlClass{Keyword}{\text{open}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8922}{\htmlId{8996}{\htmlClass{Module}{\text{HasDReps}}}}\, \,\htmlId{9005}{\htmlClass{Symbol}{\text{⦃...⦄}}}\, \,\htmlId{9011}{\htmlClass{Keyword}{\text{public}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#9020}{\htmlId{9020}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\htmlId{9034}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{9036}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{9042}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{9044}{\htmlClass{Datatype}{\text{Credential}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{9055}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{9057}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{9063}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{9065}{\htmlClass{Primitive}{\text{Type}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#9020}{\htmlId{9070}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9084}{\htmlId{9084}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{9086}{\htmlClass{Symbol}{\text{(\_}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#9091}{\htmlId{9091}{\htmlClass{Bound}{\text{expEpoch}}}}\,\,\htmlId{9099}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9101}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9084}{\htmlId{9103}{\htmlClass{Bound}{\text{e}}}}\, \,\href{Class.HasOrder.Core.html#613}{\htmlId{9105}{\htmlClass{Field Operator}{\text{≤}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9091}{\htmlId{9107}{\htmlClass{Bound}{\text{expEpoch}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#9117}{\htmlId{9117}{\htmlClass{Function}{\text{activeDRepsOf}}}}\, \,\htmlId{9131}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{9133}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#9134}{\htmlId{9134}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9136}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{9138}{\htmlClass{Primitive}{\text{Type}}}}\,\,\htmlId{9142}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{9144}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9146}{\htmlId{9146}{\htmlClass{Bound}{\text{\_}}}}\, \,\htmlId{9148}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8922}{\htmlId{9150}{\htmlClass{Record}{\text{HasDReps}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9134}{\htmlId{9159}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9161}{\htmlClass{Symbol}{\text{⦄}}}\, \,\htmlId{9163}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9134}{\htmlId{9165}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{9167}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{9169}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{9175}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8873}{\htmlId{9177}{\htmlClass{Function}{\text{DReps}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#9117}{\htmlId{9183}{\htmlClass{Function}{\text{activeDRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9197}{\htmlId{9197}{\htmlClass{Bound}{\text{a}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9199}{\htmlId{9199}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{9201}{\htmlClass{Symbol}{\text{=}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#4102}{\htmlId{9203}{\htmlClass{Function}{\text{filterᵐ}}}}\, \,\htmlId{9211}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#9020}{\htmlId{9212}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9199}{\htmlId{9226}{\htmlClass{Bound}{\text{e}}}}\,\,\htmlId{9227}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{9229}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#8971}{\htmlId{9230}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#9197}{\htmlId{9238}{\htmlClass{Bound}{\text{a}}}}\,\,\htmlId{9239}{\htmlClass{Symbol}{\text{)}}}\,