{-# OPTIONS --safe #-}

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.Conway.Specification.Gov.Base

module Ledger.Conway.Specification.Gov.Actions (gs : _) (open GovStructure gs) where


data GovRole : Type where
  CC DRep SPO : GovRole

GovRoleCredential : GovRole → Type
GovRoleCredential CC   = Credential
GovRoleCredential DRep = Credential
GovRoleCredential SPO  = KeyHash

record GovVoter : Type where


  constructor ⟦_,_⟧ᵍᵛ


  field
    gvRole       : GovRole
    gvCredential : GovRoleCredential gvRole



data VDeleg : Type where
  vDelegCredential   : Credential → VDeleg
  vDelegAbstain      : VDeleg
  vDelegNoConfidence : VDeleg

GovActionID VoteDelegs : Type
GovActionID  = TxId × ℕ
VoteDelegs   = Credential ⇀ VDeleg

record Anchor : Type where
  field
    url   : String
    hash  : DocHash

data GovActionType : Type where
  NoConfidence        : GovActionType
  UpdateCommittee     : GovActionType
  NewConstitution     : GovActionType
  TriggerHardFork     : GovActionType
  ChangePParams       : GovActionType
  TreasuryWithdrawal  : GovActionType
  Info                : GovActionType



record HasVoteDelegs {a} (A : Type a) : Type a where
  field VoteDelegsOf : A → VoteDelegs
open HasVoteDelegs ⦃...⦄ public

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


instance
  HasCast-GovAction-Sigma : HasCast GovAction (Σ GovActionType GovActionData)
  HasCast-GovAction-Sigma .cast x = x .gaType , x .gaData

  unquoteDecl Show-GovRole = derive-Show [ (quote GovRole , Show-GovRole) ]


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₁


data Vote : Type where
  yes no abstain  : Vote

record GovVote : Type where
  field
    gid         : GovActionID
    voter       : GovVoter
    vote        : Vote
    anchor      : Maybe Anchor

Policy : Type
Policy = Maybe ScriptHash

record GovProposal : Type where
  field
    action      : GovAction
    prevAction  : NeedsHash (gaType action)
    policy      : Policy
    deposit     : Coin
    returnAddr  : RwdAddr
    anchor      : Anchor

record GovVotes : Type where
  field
    gvCC   : Credential ⇀ Vote
    gvDRep : Credential ⇀ Vote
    gvSPO  : KeyHash ⇀ Vote

record GovActionState : Type where
  field
    votes       : GovVotes
    returnAddr  : RwdAddr
    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#368}{\htmlId{5567}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#5574}{\htmlId{5574}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{5582}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#5589}{\htmlId{5589}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}$
    with c ≟ c'
  ... | P.yes p = P.yes (cong $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{5644}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#5626}{\htmlId{5653}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{5654}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{5658}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{5662}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5664}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5669}{\htmlId{5669}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{5672}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5674}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5679}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{5682}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{5684}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{5689}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5669}{\htmlId{5691}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{5694}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{5698}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5511}{\htmlId{5703}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5718}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5719}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{5725}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#5732}{\htmlId{5732}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{5740}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#5747}{\htmlId{5747}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{5754}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5756}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5761}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{5763}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5511}{\htmlId{5768}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5783}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5784}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{5790}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5797}{\htmlId{5797}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{5805}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5812}{\htmlId{5812}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{5819}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5821}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5826}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{5828}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5511}{\htmlId{5833}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5848}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5849}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{5855}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5862}{\htmlId{5862}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{5870}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5877}{\htmlId{5877}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{5884}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5886}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5891}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{5893}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5511}{\htmlId{5898}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5913}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5914}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{5920}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5927}{\htmlId{5927}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{5935}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5942}{\htmlId{5942}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{5953}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5927}{\htmlId{5958}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{5960}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5942}{\htmlId{5962}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{5967}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{5971}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{5973}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5979}{\htmlId{5979}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{5981}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{5983}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{5989}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{5990}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{5997}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5979}{\htmlId{6008}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{6009}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{6013}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6017}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6019}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6024}{\htmlId{6024}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{6027}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6029}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6034}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{6037}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6039}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{6044}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6024}{\htmlId{6046}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6049}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{6053}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5511}{\htmlId{6058}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6073}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6074}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{6080}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6087}{\htmlId{6087}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{6095}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6102}{\htmlId{6102}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{6109}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6111}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6116}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{6118}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5511}{\htmlId{6123}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6138}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6139}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{6145}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6152}{\htmlId{6152}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{6160}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6167}{\htmlId{6167}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{6174}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6176}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6181}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{6183}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5511}{\htmlId{6188}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6203}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6204}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{6210}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6217}{\htmlId{6217}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{6225}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6232}{\htmlId{6232}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{6239}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6241}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6246}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{6248}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#5511}{\htmlId{6253}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{6268}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{6269}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{6275}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6282}{\htmlId{6282}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{6290}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6297}{\htmlId{6297}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{6308}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6282}{\htmlId{6313}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{6315}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6297}{\htmlId{6317}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{6322}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6326}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{6328}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6334}{\htmlId{6334}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{6336}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{6338}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{6344}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{6345}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{6352}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6334}{\htmlId{6362}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{6363}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{6367}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{6371}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6373}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6378}{\htmlId{6378}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{6381}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{6383}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{6388}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{6391}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6393}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{6398}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6378}{\htmlId{6400}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{6403}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{6407}{\htmlClass{Symbol}{\text{})}}}\,

  \,\htmlId{6413}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6425}{\htmlId{6425}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{6441}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{6443}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{6458}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{6460}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{6461}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#3270}{\htmlId{6467}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6425}{\htmlId{6477}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{6492}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{6494}{\htmlClass{Function Operator}{\text{]}}}}\,

  \,\htmlId{6499}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6511}{\htmlId{6511}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{6523}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{6525}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{6537}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{6539}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{6540}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#674}{\htmlId{6546}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6511}{\htmlId{6555}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{6566}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{6568}{\htmlClass{Function Operator}{\text{]}}}}\,



\,\href{Ledger.Conway.Specification.Gov.Actions.html#6573}{\htmlId{6573}{\htmlClass{Function}{\text{isGovVoterDRep}}}}\, \,\htmlId{6588}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#539}{\htmlId{6590}{\htmlClass{Record}{\text{GovVoter}}}}\, \,\htmlId{6599}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Maybe.html#135}{\htmlId{6601}{\htmlClass{Datatype}{\text{Maybe}}}}\, \,\href{Ledger.Core.Specification.Address.html#260}{\htmlId{6607}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6573}{\htmlId{6618}{\htmlClass{Function}{\text{isGovVoterDRep}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{6635}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6642}{\htmlId{6642}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{6648}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{6650}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6642}{\htmlId{6655}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6573}{\htmlId{6657}{\htmlClass{CatchallClause Function}{\text{isGovVoterDRep}}}}\,\,\htmlId{6671}{\htmlClass{CatchallClause}{\text{ }}}\,\,\htmlId{6672}{\htmlClass{CatchallClause Symbol}{\text{\_}}}\,              \,\htmlId{6687}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{6689}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\,

\,\href{Ledger.Conway.Specification.Gov.Actions.html#6698}{\htmlId{6698}{\htmlClass{Function}{\text{isGovVoterCredential}}}}\, \,\htmlId{6719}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#539}{\htmlId{6721}{\htmlClass{Record}{\text{GovVoter}}}}\, \,\htmlId{6730}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Maybe.html#135}{\htmlId{6732}{\htmlClass{Datatype}{\text{Maybe}}}}\, \,\href{Ledger.Core.Specification.Address.html#260}{\htmlId{6738}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6698}{\htmlId{6749}{\htmlClass{Function}{\text{isGovVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{6772}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6779}{\htmlId{6779}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{6785}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{6787}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6779}{\htmlId{6792}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6698}{\htmlId{6794}{\htmlClass{Function}{\text{isGovVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{6817}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6824}{\htmlId{6824}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{6830}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{6832}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6824}{\htmlId{6837}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6698}{\htmlId{6839}{\htmlClass{CatchallClause Function}{\text{isGovVoterCredential}}}}\,\,\htmlId{6859}{\htmlClass{CatchallClause}{\text{ }}}\,\,\htmlId{6860}{\htmlClass{CatchallClause Symbol}{\text{\_}}}\,              \,\htmlId{6875}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{6877}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\,

\,\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#1920}{\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#260}{\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#1035}{\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{6972}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.IsSet.html#916}{\htmlId{6974}{\htmlClass{Function}{\text{dom}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6956}{\htmlId{6978}{\htmlClass{Bound}{\text{x}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6886}{\htmlId{6980}{\htmlClass{CatchallClause Function}{\text{proposedCC}}}}\,\,\htmlId{6990}{\htmlClass{CatchallClause}{\text{ }}}\,\,\htmlId{6991}{\htmlClass{CatchallClause Symbol}{\text{\_}}}\,                                    \,\htmlId{7028}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.HasEmptySet.html#287}{\htmlId{7030}{\htmlClass{Field}{\text{∅}}}}\,