module Ledger.Dijkstra.Foreign.Gov.Actions where
open import Data.Rational using (ℚ)
open import Foreign.Convertible
open import Foreign.Convertible.Deriving
open import Foreign.HaskellTypes
open import Foreign.HaskellTypes.Deriving
open import Ledger.Prelude
open import Ledger.Prelude.Foreign.HSTypes
open import Ledger.Dijkstra.Foreign.HSStructures
open import Ledger.Dijkstra.Foreign.PParams
open import Ledger.Core.Foreign.Address
open import Ledger.Core.Specification.ProtocolVersion
data GovAction' : Type where
NoConfidence : GovAction'
UpdateCommittee : (Credential ⇀ Epoch) → ℙ Credential → ℚ → GovAction'
NewConstitution : ADHash → 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.Dijkstra.Specification.Gov.Actions.html#625}{\htmlId{1209}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{1231}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → NoConfidence
.to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#663}{\htmlId{1272}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{1294}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1295}{\htmlId{1295}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1299}{\htmlId{1299}{\htmlClass{Bound}{\text{s}}}}\, , \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1303}{\htmlId{1303}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1304}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ → UpdateCommittee m s q
.to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#701}{\htmlId{1344}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1366}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1367}{\htmlId{1367}{\htmlClass{Bound}{\text{h}}}}\, , \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1371}{\htmlId{1371}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{1372}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ → NewConstitution h s
.to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#739}{\htmlId{1414}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1436}{\htmlId{1436}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$ → TriggerHardFork v
.to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#777}{\htmlId{1482}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1504}{\htmlId{1504}{\htmlClass{Bound}{\text{u}}}}\, \end{pmatrix}$ → ChangePParams u
.to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#815}{\htmlId{1548}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1570}{\htmlId{1570}{\htmlClass{Bound}{\text{w}}}}\, \end{pmatrix}$ → TreasuryWithdrawal w
.to $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#853}{\htmlId{1619}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{1641}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ → Info
.from NoConfidence → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#625}{\htmlId{1704}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{1726}{\htmlClass{InductiveConstructor}{\text{tt}}}}\, \end{pmatrix}$
.from (UpdateCommittee m s q) → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#663}{\htmlId{1782}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{1804}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1769}{\htmlId{1805}{\htmlClass{Bound}{\text{m}}}}\, , \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1771}{\htmlId{1809}{\htmlClass{Bound}{\text{s}}}}\, , \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1773}{\htmlId{1813}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1814}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
.from (NewConstitution h s) → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#701}{\htmlId{1860}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1882}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1847}{\htmlId{1883}{\htmlClass{Bound}{\text{h}}}}\, , \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1849}{\htmlId{1887}{\htmlClass{Bound}{\text{s}}}}\,\,\htmlId{1888}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
.from (TriggerHardFork v) → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#739}{\htmlId{1938}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#1925}{\htmlId{1960}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$
.from (ChangePParams u) → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#777}{\htmlId{2016}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#2001}{\htmlId{2038}{\htmlClass{Bound}{\text{u}}}}\, \end{pmatrix}$
.from (TreasuryWithdrawal w) → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#815}{\htmlId{2094}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Dijkstra.Foreign.Gov.Actions.html#2084}{\htmlId{2116}{\htmlClass{Bound}{\text{w}}}}\, \end{pmatrix}$
.from Info → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#853}{\htmlId{2172}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\href{Agda.Builtin.Unit.html#212}{\htmlId{2194}{\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'