module Ledger.Conway.Foreign.HSLedger.GovernanceActions where
open import Data.Rational using (ℚ)
open import Ledger.Conway.Foreign.HSLedger.Address
open import Ledger.Conway.Foreign.HSLedger.BaseTypes
open import Ledger.Conway.Foreign.HSLedger.PParams
open import Ledger.Conway.Types.GovStructure
open import Ledger.Conway.GovernanceActions govStructure using (Vote) public
DocHash = GovStructure.DocHash govStructure
data GovAction' : Type where
NoConfidence : GovAction'
UpdateCommittee : (Credential ⇀ Epoch) → ℙ Credential → ℚ → GovAction'
NewConstitution : DocHash → Maybe ScriptHash → GovAction'
TriggerHF : ProtVer → GovAction'
ChangePParams : PParamsUpdate → GovAction'
TreasuryWdrl : (RwdAddr ⇀ Coin) → GovAction'
Info : GovAction'
instance
mkGovAction' : Convertible GovAction GovAction'
mkGovAction' = λ where
.to $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#758}{\htmlId{1119}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{1137}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → NoConfidence
.to $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#793}{\htmlId{1178}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1197}{\htmlId{1197}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1201}{\htmlId{1201}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1205}{\htmlId{1205}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$ → (UpdateCommittee m p q)
.to $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#828}{\htmlId{1248}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1267}{\htmlId{1267}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1272}{\htmlId{1272}{\htmlClass{Bound}{\text{s}}}}\, ) \end{pmatrix}$ → (NewConstitution dh s)
.to $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#863}{\htmlId{1317}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1335}{\htmlId{1335}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ → (TriggerHF p)
.to $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#898}{\htmlId{1377}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1395}{\htmlId{1395}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$ → (ChangePParams pu)
.to $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#933}{\htmlId{1442}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1460}{\htmlId{1460}{\htmlClass{Bound}{\text{m}}}}\, \end{pmatrix}$ → ((TreasuryWdrl m))
.to $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#968}{\htmlId{1507}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{1525}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → Info
.from NoConfidence → $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#758}{\htmlId{1590}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{1608}{\htmlClass{InductiveConstructor}{\text{tt}}}}\, \end{pmatrix}$
.from (UpdateCommittee m p q) → $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#793}{\htmlId{1666}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1651}{\htmlId{1685}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1653}{\htmlId{1689}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1655}{\htmlId{1693}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$
.from (NewConstitution dh s) → $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#828}{\htmlId{1742}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ (\,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1727}{\htmlId{1761}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1730}{\htmlId{1766}{\htmlClass{Bound}{\text{s}}}}\,) \end{pmatrix}$
.from (TriggerHF p) → $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#863}{\htmlId{1818}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1797}{\htmlId{1836}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$
.from (ChangePParams pu) → $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#898}{\htmlId{1894}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1877}{\htmlId{1912}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$
.from (TreasuryWdrl m) → $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#933}{\htmlId{1970}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.GovernanceActions.html#1952}{\htmlId{1988}{\htmlClass{Bound}{\text{m}}}}\, \end{pmatrix}$
.from Info → $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#968}{\htmlId{2046}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{2053}{\htmlClass{InductiveConstructor}{\text{tt}}}}\, \end{pmatrix}$
HsTy-GovAction' = autoHsType GovAction' ⊣ withName "GovAction"
Conv-GovAction' = autoConvert GovAction'
HsTy-GovAction = MkHsType GovAction (HsType GovAction')
Conv-GovAction = mkGovAction' ⨾ Conv-GovAction'