Actions
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 : (RwdAddr ⇀ Treasury) → GovAction'
Info : GovAction'
instance
mkGovAction' : Convertible GovAction GovAction'
mkGovAction' = λ where
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1877}{\htmlId{1249}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{1271}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → NoConfidence
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1915}{\htmlId{1312}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{1334}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1335}{\htmlId{1335}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1339}{\htmlId{1339}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1343}{\htmlId{1343}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1344}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ → (UpdateCommittee m p q)
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1953}{\htmlId{1386}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1408}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1409}{\htmlId{1409}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1414}{\htmlId{1414}{\htmlClass{Bound}{\text{s}}}}\, \,\htmlId{1416}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ → (NewConstitution dh s)
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1991}{\htmlId{1459}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1481}{\htmlId{1481}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ → (TriggerHardFork p)
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2029}{\htmlId{1529}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1551}{\htmlId{1551}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$ → (ChangePParams pu)
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2067}{\htmlId{1598}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1620}{\htmlId{1620}{\htmlClass{Bound}{\text{m}}}}\, \end{pmatrix}$ → ((TreasuryWithdrawal m))
.to $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2105}{\htmlId{1673}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{1695}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → Info
.from NoConfidence → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1877}{\htmlId{1758}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{1780}{\htmlClass{InductiveConstructor}{\text{tt}}}}\, \end{pmatrix}$
.from (UpdateCommittee m p q) → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1915}{\htmlId{1836}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{1858}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1823}{\htmlId{1859}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1825}{\htmlId{1863}{\htmlClass{Bound}{\text{p}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1827}{\htmlId{1867}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1868}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
.from (NewConstitution dh s) → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1953}{\htmlId{1914}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1936}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1901}{\htmlId{1937}{\htmlClass{Bound}{\text{dh}}}}\, , \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1904}{\htmlId{1942}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{1943}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
.from (TriggerHardFork p) → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1991}{\htmlId{1992}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#1979}{\htmlId{2014}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$
.from (ChangePParams pu) → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2029}{\htmlId{2070}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#2055}{\htmlId{2092}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$
.from (TreasuryWithdrawal m) → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2067}{\htmlId{2148}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Gov.Actions.html#2138}{\htmlId{2170}{\htmlClass{Bound}{\text{m}}}}\, \end{pmatrix}$
.from Info → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2105}{\htmlId{2226}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{2248}{\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'