{-# 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


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-GovActionType = derive-DecEq ((quote GovActionType , DecEq-GovActionType) ∷ [])
  unquoteDecl DecEq-GovRole       = derive-DecEq ((quote GovRole , DecEq-GovRole) ∷ [])
  unquoteDecl DecEq-Vote          = derive-DecEq ((quote Vote    , DecEq-Vote)    ∷ [])
  unquoteDecl DecEq-VDeleg        = derive-DecEq ((quote VDeleg  , DecEq-VDeleg)  ∷ [])

  DecEq-GovVoter : DecEq GovVoter
  DecEq-GovVoter ._≟_ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{5596}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#5603}{\htmlId{5603}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{5611}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#5618}{\htmlId{5618}{\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{5673}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#5655}{\htmlId{5682}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{5683}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{5687}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{5691}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5693}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5698}{\htmlId{5698}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{5701}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5703}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5708}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{5711}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{5713}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{5718}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5698}{\htmlId{5720}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{5723}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{5727}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5540}{\htmlId{5732}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5747}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5748}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{5754}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#5761}{\htmlId{5761}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{5769}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#5776}{\htmlId{5776}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{5783}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5785}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5790}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{5792}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5540}{\htmlId{5797}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5812}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5813}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{5819}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5826}{\htmlId{5826}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{5834}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5841}{\htmlId{5841}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{5848}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5850}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5855}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{5857}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5540}{\htmlId{5862}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5877}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5878}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{5884}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5891}{\htmlId{5891}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{5899}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5906}{\htmlId{5906}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{5913}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5915}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5920}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{5922}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5540}{\htmlId{5927}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5942}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5943}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{5949}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5956}{\htmlId{5956}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{5964}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5971}{\htmlId{5971}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{5982}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5956}{\htmlId{5987}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{5989}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5971}{\htmlId{5991}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{5996}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6000}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{6002}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6008}{\htmlId{6008}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{6010}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{6012}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{6018}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{6019}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{6026}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6008}{\htmlId{6037}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{6038}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{6042}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6046}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6048}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6053}{\htmlId{6053}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{6056}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6058}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6063}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{6066}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6068}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{6073}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6053}{\htmlId{6075}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6078}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{6082}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5540}{\htmlId{6087}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6102}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6103}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{6109}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6116}{\htmlId{6116}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{6124}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6131}{\htmlId{6131}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{6138}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6140}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6145}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{6147}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5540}{\htmlId{6152}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6167}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6168}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{6174}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6181}{\htmlId{6181}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{6189}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6196}{\htmlId{6196}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{6203}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6205}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6210}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{6212}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5540}{\htmlId{6217}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6232}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6233}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{6239}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6246}{\htmlId{6246}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{6254}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6261}{\htmlId{6261}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{6268}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6270}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6275}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{6277}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5540}{\htmlId{6282}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6297}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6298}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{6304}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6311}{\htmlId{6311}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{6319}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6326}{\htmlId{6326}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{6337}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6311}{\htmlId{6342}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{6344}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6326}{\htmlId{6346}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{6351}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6355}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{6357}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6363}{\htmlId{6363}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{6365}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{6367}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{6373}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{6374}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{6381}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6363}{\htmlId{6391}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{6392}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{6396}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6400}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6402}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6407}{\htmlId{6407}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{6410}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6412}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6417}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{6420}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6422}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{6427}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6407}{\htmlId{6429}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6432}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{6436}{\htmlClass{Symbol}{\text{})}}}\,

  \,\htmlId{6442}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6454}{\htmlId{6454}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{6470}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{6472}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{6487}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{6489}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{6490}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#2294}{\htmlId{6496}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6454}{\htmlId{6506}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{6521}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{6523}{\htmlClass{Function Operator}{\text{]}}}}\,

  \,\htmlId{6528}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6540}{\htmlId{6540}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{6552}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{6554}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{6566}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{6568}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{6569}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#2570}{\htmlId{6575}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6540}{\htmlId{6584}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{6595}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{6597}{\htmlClass{Function Operator}{\text{]}}}}\,


\,\href{Ledger.Conway.Specification.Gov.Actions.html#6601}{\htmlId{6601}{\htmlClass{Function}{\text{isGovVoterDRep}}}}\, \,\htmlId{6616}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#2082}{\htmlId{6618}{\htmlClass{Record}{\text{GovVoter}}}}\, \,\htmlId{6627}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Maybe.html#135}{\htmlId{6629}{\htmlClass{Datatype}{\text{Maybe}}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{6635}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6601}{\htmlId{6646}{\htmlClass{Function}{\text{isGovVoterDRep}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{6663}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6670}{\htmlId{6670}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{6676}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{6678}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6670}{\htmlId{6683}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6601}{\htmlId{6685}{\htmlClass{CatchallClause Function}{\text{isGovVoterDRep}}}}\,\,\htmlId{6699}{\htmlClass{CatchallClause}{\text{ }}}\,\,\htmlId{6700}{\htmlClass{CatchallClause Symbol}{\text{\_}}}\, \,\htmlId{6702}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{6704}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\,

\,\href{Ledger.Conway.Specification.Gov.Actions.html#6713}{\htmlId{6713}{\htmlClass{Function}{\text{govVoterCredential}}}}\, \,\htmlId{6732}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#2082}{\htmlId{6734}{\htmlClass{Record}{\text{GovVoter}}}}\, \,\htmlId{6743}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{6745}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6713}{\htmlId{6756}{\htmlClass{Function}{\text{govVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#369}{\htmlId{6777}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6784}{\htmlId{6784}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix} \,\htmlId{6791}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6784}{\htmlId{6793}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6713}{\htmlId{6795}{\htmlClass{Function}{\text{govVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#372}{\htmlId{6816}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6823}{\htmlId{6823}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix} \,\htmlId{6830}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6823}{\htmlId{6832}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6713}{\htmlId{6834}{\htmlClass{Function}{\text{govVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#377}{\htmlId{6855}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6862}{\htmlId{6862}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix} \,\htmlId{6869}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Core.Specification.Address.html#285}{\htmlId{6871}{\htmlClass{InductiveConstructor}{\text{KeyHashObj}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6862}{\htmlId{6882}{\htmlClass{Bound}{\text{kh}}}}\,

\,\href{Ledger.Conway.Specification.Gov.Actions.html#6886}{\htmlId{6886}{\htmlClass{Function}{\text{proposedCC}}}}\, \,\htmlId{6897}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#1454}{\htmlId{6899}{\htmlClass{Record}{\text{GovAction}}}}\, \,\htmlId{6909}{\htmlClass{Symbol}{\text{→}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#488}{\htmlId{6911}{\htmlClass{Function Operator}{\text{ℙ}}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{6913}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6886}{\htmlId{6924}{\htmlClass{Function}{\text{proposedCC}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#694}{\htmlId{6937}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, , \,\htmlId{6955}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#6956}{\htmlId{6956}{\htmlClass{Bound}{\text{x}}}}\, , \,\htmlId{6960}{\htmlClass{Symbol}{\text{\_}}}\, , \,\htmlId{6964}{\htmlClass{Symbol}{\text{\_)}}}\, \end{pmatrix} \,\htmlId{6971}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.IsSet.html#916}{\htmlId{6973}{\htmlClass{Function}{\text{dom}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6956}{\htmlId{6977}{\htmlClass{Bound}{\text{x}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6886}{\htmlId{6979}{\htmlClass{CatchallClause Function}{\text{proposedCC}}}}\,\,\htmlId{6989}{\htmlClass{CatchallClause}{\text{ }}}\,\,\htmlId{6990}{\htmlClass{CatchallClause Symbol}{\text{\_}}}\, \,\htmlId{6992}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.HasEmptySet.html#287}{\htmlId{6994}{\htmlClass{Field}{\text{∅}}}}\,


\,\href{Ledger.Conway.Specification.Gov.Actions.html#6998}{\htmlId{6998}{\htmlClass{Function}{\text{DReps}}}}\, \,\htmlId{7004}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{7006}{\htmlClass{Primitive}{\text{Type}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6998}{\htmlId{7011}{\htmlClass{Function}{\text{DReps}}}}\, \,\htmlId{7017}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{7019}{\htmlClass{Datatype}{\text{Credential}}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#633}{\htmlId{7030}{\htmlClass{Function Operator}{\text{⇀}}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{7032}{\htmlClass{Function}{\text{Epoch}}}}\,


\,\htmlId{7040}{\htmlClass{Keyword}{\text{record}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7047}{\htmlId{7047}{\htmlClass{Record}{\text{HasDReps}}}}\, \,\htmlId{7056}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#7057}{\htmlId{7057}{\htmlClass{Bound}{\text{a}}}}\,\,\htmlId{7058}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7060}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#7061}{\htmlId{7061}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{7063}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{7065}{\htmlClass{Primitive}{\text{Type}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7057}{\htmlId{7070}{\htmlClass{Bound}{\text{a}}}}\,\,\htmlId{7071}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{7073}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{7075}{\htmlClass{Primitive}{\text{Type}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7057}{\htmlId{7080}{\htmlClass{Bound}{\text{a}}}}\, \,\htmlId{7082}{\htmlClass{Keyword}{\text{where}}}\,
  \,\htmlId{7090}{\htmlClass{Keyword}{\text{field}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7096}{\htmlId{7096}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\htmlId{7104}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7061}{\htmlId{7106}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{7108}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6998}{\htmlId{7110}{\htmlClass{Function}{\text{DReps}}}}\,
\,\htmlId{7116}{\htmlClass{Keyword}{\text{open}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7047}{\htmlId{7121}{\htmlClass{Module}{\text{HasDReps}}}}\, \,\htmlId{7130}{\htmlClass{Symbol}{\text{⦃...⦄}}}\, \,\htmlId{7136}{\htmlClass{Keyword}{\text{public}}}\,


\,\href{Ledger.Conway.Specification.Gov.Actions.html#7145}{\htmlId{7145}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\htmlId{7159}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{7161}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{7167}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Address.html#259}{\htmlId{7169}{\htmlClass{Datatype}{\text{Credential}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{7180}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{7182}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{7188}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{7190}{\htmlClass{Primitive}{\text{Type}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7145}{\htmlId{7195}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7209}{\htmlId{7209}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{7211}{\htmlClass{Symbol}{\text{(\_}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#7216}{\htmlId{7216}{\htmlClass{Bound}{\text{expEpoch}}}}\,\,\htmlId{7224}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{7226}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7209}{\htmlId{7228}{\htmlClass{Bound}{\text{e}}}}\, \,\href{Class.HasOrder.Core.html#613}{\htmlId{7230}{\htmlClass{Field Operator}{\text{≤}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7216}{\htmlId{7232}{\htmlClass{Bound}{\text{expEpoch}}}}\,

\,\href{Ledger.Conway.Specification.Gov.Actions.html#7242}{\htmlId{7242}{\htmlClass{Function}{\text{activeDRepsOf}}}}\, \,\htmlId{7256}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{7258}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#7259}{\htmlId{7259}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{7261}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{7263}{\htmlClass{Primitive}{\text{Type}}}}\,\,\htmlId{7267}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{7269}{\htmlClass{Symbol}{\text{⦃}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7271}{\htmlId{7271}{\htmlClass{Bound}{\text{\_}}}}\, \,\htmlId{7273}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7047}{\htmlId{7275}{\htmlClass{Record}{\text{HasDReps}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7259}{\htmlId{7284}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{7286}{\htmlClass{Symbol}{\text{⦄}}}\, \,\htmlId{7288}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7259}{\htmlId{7290}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{7292}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Core.Specification.Epoch.html#646}{\htmlId{7294}{\htmlClass{Function}{\text{Epoch}}}}\, \,\htmlId{7300}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6998}{\htmlId{7302}{\htmlClass{Function}{\text{DReps}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#7242}{\htmlId{7308}{\htmlClass{Function}{\text{activeDRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7322}{\htmlId{7322}{\htmlClass{Bound}{\text{a}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7324}{\htmlId{7324}{\htmlClass{Bound}{\text{e}}}}\, \,\htmlId{7326}{\htmlClass{Symbol}{\text{=}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#4102}{\htmlId{7328}{\htmlClass{Function}{\text{filterᵐ}}}}\, \,\htmlId{7336}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#7145}{\htmlId{7337}{\htmlClass{Function}{\text{activeInEpoch}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7324}{\htmlId{7351}{\htmlClass{Bound}{\text{e}}}}\,\,\htmlId{7352}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{7354}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#7096}{\htmlId{7355}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7322}{\htmlId{7363}{\htmlClass{Bound}{\text{a}}}}\,\,\htmlId{7364}{\htmlClass{Symbol}{\text{)}}}\,