Cert
module Ledger.Conway.Foreign.HSLedger.Cert where
open import Ledger.Conway.Foreign.HSLedger.BaseTypes hiding (CertEnv; DCert) renaming (⟦_,_,_⟧ᶜˢ to ⟦_,_,_⟧ᶜˢ'; CertState to CertState')
open import Ledger.Conway.Foreign.HSLedger.Certs
open import Ledger.Conway.Conformance.Certs.Properties govStructure
using ( Computational-CERT
; Computational-CERTS
)
open import Ledger.Conway.Conformance.Certs govStructure
instance
HsTy-CertState = autoHsType CertState ⊣ withConstructor "MkCertState"
Conv-CertState = autoConvert CertState
Conv-CertState-CertState' : Convertible CertState CertState'
Conv-CertState-CertState' .to $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#873}{\htmlId{873}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#882}{\htmlId{882}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#891}{\htmlId{891}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Foreign.Convertible.html#230}{\htmlId{909}{\htmlClass{Field}{\text{to}}}}\, \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#873}{\htmlId{912}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#882}{\htmlId{921}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Foreign.Convertible.html#230}{\htmlId{930}{\htmlClass{Field}{\text{to}}}}\, \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#891}{\htmlId{933}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix}$
Conv-CertState-CertState' .from $\begin{pmatrix} \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#981}{\htmlId{981}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#990}{\htmlId{990}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#999}{\htmlId{999}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \,\href{Foreign.Convertible.html#251}{\htmlId{1015}{\htmlClass{Field}{\text{from}}}}\, \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#981}{\htmlId{1020}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#990}{\htmlId{1029}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Foreign.Convertible.html#251}{\htmlId{1038}{\htmlClass{Field}{\text{from}}}}\, \,\href{Ledger.Conway.Foreign.HSLedger.Cert.html#999}{\htmlId{1043}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix}$
certs-step : HsType (CertEnv → CertState → List DCert → ComputationResult String CertState)
certs-step = to (compute Computational-CERTS)
{-# COMPILE GHC certs-step as certsStep #-}
cert-step : HsType (CertEnv → CertState → DCert → ComputationResult String CertState)
cert-step = to (compute Computational-CERT)
{-# COMPILE GHC cert-step as certStep #-}