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

record GovProposal : Type where
  field
    action      : GovAction
    prevAction  : NeedsHash (gaType action)
    policy      : Maybe ScriptHash
    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)


instance
  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{4935}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#4942}{\htmlId{4942}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{4950}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#4957}{\htmlId{4957}{\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{5012}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#4994}{\htmlId{5021}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{5022}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{5026}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{5030}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5032}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5037}{\htmlId{5037}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{5040}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5042}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5047}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{5050}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{5052}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{5057}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5037}{\htmlId{5059}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{5062}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{5066}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#4879}{\htmlId{5071}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5086}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5087}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{5093}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#5100}{\htmlId{5100}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{5108}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#5115}{\htmlId{5115}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{5122}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5124}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5129}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{5131}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#4879}{\htmlId{5136}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5151}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5152}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{5158}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5165}{\htmlId{5165}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{5173}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5180}{\htmlId{5180}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{5187}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5189}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5194}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{5196}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#4879}{\htmlId{5201}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5216}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5217}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{5223}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5230}{\htmlId{5230}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{5238}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5245}{\htmlId{5245}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{5252}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5254}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5259}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{5261}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#4879}{\htmlId{5266}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5281}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5282}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{5288}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5295}{\htmlId{5295}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{5303}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5310}{\htmlId{5310}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{5321}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5295}{\htmlId{5326}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{5328}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5310}{\htmlId{5330}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{5335}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{5339}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{5341}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5347}{\htmlId{5347}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{5349}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{5351}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{5357}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{5358}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{5365}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5347}{\htmlId{5376}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{5377}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{5381}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{5385}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5387}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5392}{\htmlId{5392}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{5395}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5397}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5402}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{5405}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{5407}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{5412}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5392}{\htmlId{5414}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{5417}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{5421}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#4879}{\htmlId{5426}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5441}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5442}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{5448}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5455}{\htmlId{5455}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{5463}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5470}{\htmlId{5470}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{5477}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5479}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5484}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{5486}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#4879}{\htmlId{5491}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5506}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5507}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{5513}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5520}{\htmlId{5520}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{5528}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5535}{\htmlId{5535}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{5542}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5544}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5549}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{5551}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#4879}{\htmlId{5556}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5571}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5572}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{5578}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5585}{\htmlId{5585}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{5593}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5600}{\htmlId{5600}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{5607}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5609}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5614}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{5616}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#4879}{\htmlId{5621}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{5636}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{5637}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{5643}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5650}{\htmlId{5650}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{5658}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5665}{\htmlId{5665}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{5676}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5650}{\htmlId{5681}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{5683}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5665}{\htmlId{5685}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{5690}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{5694}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{5696}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5702}{\htmlId{5702}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{5704}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{5706}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{5712}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{5713}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#376}{\htmlId{5720}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5702}{\htmlId{5730}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{5731}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{5735}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{5739}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5741}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5746}{\htmlId{5746}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{5749}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{5751}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{5756}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{5759}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{5761}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{5766}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5746}{\htmlId{5768}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{5771}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{5775}{\htmlClass{Symbol}{\text{})}}}\,

  \,\htmlId{5781}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5793}{\htmlId{5793}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{5809}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{5811}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{5826}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{5828}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{5829}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#3270}{\htmlId{5835}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5793}{\htmlId{5845}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{5860}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{5862}{\htmlClass{Function Operator}{\text{]}}}}\,

  \,\htmlId{5867}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#5879}{\htmlId{5879}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{5891}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{5893}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{5905}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{5907}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{5908}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#674}{\htmlId{5914}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#5879}{\htmlId{5923}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{5934}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{5936}{\htmlClass{Function Operator}{\text{]}}}}\,



\,\href{Ledger.Conway.Specification.Gov.Actions.html#5941}{\htmlId{5941}{\htmlClass{Function}{\text{isGovVoterDRep}}}}\, \,\htmlId{5956}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#539}{\htmlId{5958}{\htmlClass{Record}{\text{GovVoter}}}}\, \,\htmlId{5967}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Maybe.html#135}{\htmlId{5969}{\htmlClass{Datatype}{\text{Maybe}}}}\, \,\href{Ledger.Core.Specification.Address.html#260}{\htmlId{5975}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#5941}{\htmlId{5986}{\htmlClass{Function}{\text{isGovVoterDRep}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{6003}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6010}{\htmlId{6010}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{6016}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{6018}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6010}{\htmlId{6023}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#5941}{\htmlId{6025}{\htmlClass{CatchallClause Function}{\text{isGovVoterDRep}}}}\,\,\htmlId{6039}{\htmlClass{CatchallClause}{\text{ }}}\,\,\htmlId{6040}{\htmlClass{CatchallClause Symbol}{\text{\_}}}\,              \,\htmlId{6055}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{6057}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\,

\,\href{Ledger.Conway.Specification.Gov.Actions.html#6066}{\htmlId{6066}{\htmlClass{Function}{\text{isGovVoterCredential}}}}\, \,\htmlId{6087}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#539}{\htmlId{6089}{\htmlClass{Record}{\text{GovVoter}}}}\, \,\htmlId{6098}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Agda.Builtin.Maybe.html#135}{\htmlId{6100}{\htmlClass{Datatype}{\text{Maybe}}}}\, \,\href{Ledger.Core.Specification.Address.html#260}{\htmlId{6106}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6066}{\htmlId{6117}{\htmlClass{Function}{\text{isGovVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#368}{\htmlId{6140}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6147}{\htmlId{6147}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{6153}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{6155}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6147}{\htmlId{6160}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6066}{\htmlId{6162}{\htmlClass{Function}{\text{isGovVoterCredential}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#371}{\htmlId{6185}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#6192}{\htmlId{6192}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \,\htmlId{6198}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{6200}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6192}{\htmlId{6205}{\htmlClass{Bound}{\text{c}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6066}{\htmlId{6207}{\htmlClass{CatchallClause Function}{\text{isGovVoterCredential}}}}\,\,\htmlId{6227}{\htmlClass{CatchallClause}{\text{ }}}\,\,\htmlId{6228}{\htmlClass{CatchallClause Symbol}{\text{\_}}}\,              \,\htmlId{6243}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{6245}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\,

\,\href{Ledger.Conway.Specification.Gov.Actions.html#6254}{\htmlId{6254}{\htmlClass{Function}{\text{proposedCC}}}}\, \,\htmlId{6265}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#1920}{\htmlId{6267}{\htmlClass{Record}{\text{GovAction}}}}\, \,\htmlId{6277}{\htmlClass{Symbol}{\text{→}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#488}{\htmlId{6279}{\htmlClass{Function Operator}{\text{ℙ}}}}\, \,\href{Ledger.Core.Specification.Address.html#260}{\htmlId{6281}{\htmlClass{Datatype}{\text{Credential}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6254}{\htmlId{6292}{\htmlClass{Function}{\text{proposedCC}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1035}{\htmlId{6305}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, , \,\htmlId{6323}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#6324}{\htmlId{6324}{\htmlClass{Bound}{\text{x}}}}\, , \,\htmlId{6328}{\htmlClass{Symbol}{\text{\_}}}\, , \,\htmlId{6332}{\htmlClass{Symbol}{\text{\_)}}}\, \end{pmatrix}  \,\htmlId{6340}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.IsSet.html#916}{\htmlId{6342}{\htmlClass{Function}{\text{dom}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#6324}{\htmlId{6346}{\htmlClass{Bound}{\text{x}}}}\,
\,\href{Ledger.Conway.Specification.Gov.Actions.html#6254}{\htmlId{6348}{\htmlClass{CatchallClause Function}{\text{proposedCC}}}}\,\,\htmlId{6358}{\htmlClass{CatchallClause}{\text{ }}}\,\,\htmlId{6359}{\htmlClass{CatchallClause Symbol}{\text{\_}}}\,                                    \,\htmlId{6396}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Class.HasEmptySet.html#287}{\htmlId{6398}{\htmlClass{Field}{\text{∅}}}}\,