module Ledger.Conway.Foreign.HSLedger.Gov.Actions 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.Specification.Gov.Base
open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote) public
DocHash = GovStructure.DocHash govStructure
data GovAction' : Type where
NoConfidence : GovAction'
UpdateCommittee : (Credential ⇀ Epoch) → ℙ Credential → ℚ → GovAction'
NewConstitution : DocHash → Maybe ScriptHash → GovAction'
TriggerHardFork : ProtVer → GovAction'
ChangePParams : PParamsUpdate → GovAction'
TreasuryWithdrawal : (RewardAddress ⇀ Treasury) → GovAction'
Info : GovAction'
instance
mkGovAction' : Convertible GovAction GovAction'
mkGovAction' = λ where
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#656}{\htmlId{1146}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{1168}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → NoConfidence
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#694}{\htmlId{1209}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{1231}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1232}{\htmlId{1232}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1236}{\htmlId{1236}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1240}{\htmlId{1240}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1241}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ → (UpdateCommittee m p q)
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#732}{\htmlId{1283}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1305}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1306}{\htmlId{1306}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1311}{\htmlId{1311}{\htmlClass{Bound}{\text{s}}}}\, \,\htmlId{1313}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ → (NewConstitution dh s)
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#770}{\htmlId{1356}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1378}{\htmlId{1378}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ → (TriggerHardFork p)
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#808}{\htmlId{1426}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1448}{\htmlId{1448}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$ → (ChangePParams pu)
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#846}{\htmlId{1495}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1517}{\htmlId{1517}{\htmlClass{Bound}{\text{m}}}}\, \end{pmatrix}$ → ((TreasuryWithdrawal m))
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#884}{\htmlId{1570}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{1592}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → Info
.from NoConfidence → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#656}{\htmlId{1655}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{1677}{\htmlClass{InductiveConstructor}{\text{tt}}}}\, \end{pmatrix}$
.from (UpdateCommittee m p q) → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#694}{\htmlId{1733}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{1755}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1720}{\htmlId{1756}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1722}{\htmlId{1760}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1724}{\htmlId{1764}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1765}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
.from (NewConstitution dh s) → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#732}{\htmlId{1811}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1833}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1798}{\htmlId{1834}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1801}{\htmlId{1839}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{1840}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
.from (TriggerHardFork p) → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#770}{\htmlId{1889}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1876}{\htmlId{1911}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$
.from (ChangePParams pu) → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#808}{\htmlId{1967}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1952}{\htmlId{1989}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$
.from (TreasuryWithdrawal m) → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#846}{\htmlId{2045}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#2035}{\htmlId{2067}{\htmlClass{Bound}{\text{m}}}}\, \end{pmatrix}$
.from Info → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#884}{\htmlId{2123}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{2145}{\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'