Formal Ledger Specification
Ledger
Initializing search
    GitHub
    • Navigation
    GitHub
      • Home
      • Guide for Contributors
        • Notation
      • Ledger
        • Introduction
        • Prelude
          • Base
          • Instances
        • Conway
          • Abstract
          • Address
          • BaseTypes
          • Certs
            • Properties
              • PoV
              • PoVLemmas
              • VoteDelegsVDeleg
          • Chain
            • Properties
              • CredDepsEqualDomRwds
              • EpochStep
              • GovDepsMatch
              • PParamsWellFormed
          • Crypto
          • Enact
            • Properties
          • Epoch
            • Properties
              • ConstRwds
              • GovDepsMatch
              • NoPropSameDReps
          • Fees
          • Gov
            • Base
            • Actions
            • Properties
              • ChangePPGroup
          • Ledger.Ledger
            • Properties
              • GovDepsMatch
              • PoV
          • PParams
          • Properties
          • Ratify
            • Properties
          • Rewards
          • Script
            • Base
            • Timelock
            • Validation
            • Base
            • Coin
            • ValueSet
            • ValueVector
          • Transaction
            • Epoch
            • Numeric
              • UnitInterval
              • PositiveNat
          • Utxo
            • Properties
              • MinSpend
              • PoV
          • Utxow
            • Properties
            • ExternalFunctions
            • HSLedger
              • Address
              • BaseTypes
              • Cert
              • Certs
              • Chain
              • Core
              • Enact
              • Epoch
              • ExternalStructures
              • Gov
                • Core
                • Actions
              • Ledger
              • NewEpoch
              • PParams
              • Ratify
              • Transaction
              • Utxo
            • HSTypes
            • Util
            • Certs
              • Properties
            • Chain
              • Properties
            • Epoch
              • Properties
            • Equivalence
              • Bisimilarity
              • Certs
              • Convert
              • Deposits
              • Map
              • Utxo
            • Gov
            • Ledger
              • Properties
            • Properties
            • Script
            • Utxo
              • Properties
            • Utxow
              • Properties
            • Examples
              • HelloWorld
              • SucceedIfNumber
            • LedgerImplementation
            • Lib
            • Prelude
            • StructuredContracts
        • ConwaySafe
          • HasCoin
        • PreConway
            • NewPP
              • Properties
            • PPUp
              • Properties
          • NewPP
            • Properties
          • PPUp
            • Properties
        • Convertible
          • Deriving
          • DerivingTest
        • HaskellTypes
          • Deriving
        • EssentialAgda
        • Agda Prelude
            • ComputationalRelation
            • HasSubset
            • HasSubtract
              • Instance
            • Hashable
            • STS
          • MyDebugOptions

    Ledger

    module Ledger.Conway.Foreign.HSLedger.Ledger where
    
    open import Ledger.Conway.Foreign.HSLedger.Address
    open import Ledger.Conway.Foreign.HSLedger.BaseTypes
    open import Ledger.Conway.Foreign.HSLedger.Certs
    open import Ledger.Conway.Foreign.HSLedger.Enact
    open import Ledger.Conway.Foreign.HSLedger.Gov
    open import Ledger.Conway.Foreign.HSLedger.PParams
    open import Ledger.Conway.Foreign.HSLedger.Transaction
    open import Ledger.Conway.Foreign.HSLedger.Utxo
    open import Ledger.Conway.Foreign.HSLedger.Cert
    
    open import Ledger.Conway.Conformance.Ledger it it
    open import Ledger.Conway.Conformance.Ledger.Properties it it
    
    instance
      HsTy-LEnv = autoHsType LEnv ⊣ withConstructor "MkLEnv"
                                  • fieldPrefix "le"
      Conv-LEnv = autoConvert LEnv
    
      HsTy-LState = autoHsType LState ⊣ withConstructor "MkLState"
      Conv-LState = autoConvert LState
    
    ledger-step : HsType (LEnv → LState → Tx → ComputationResult String LState)
    ledger-step = to (compute Computational-LEDGER)
    
    {-# COMPILE GHC ledger-step as ledgerStep #-}
    
    ledgers-step : HsType (LEnv → LState → List Tx → ComputationResult String LState)
    ledgers-step = to (compute Computational-LEDGERS)
    
    {-# COMPILE GHC ledgers-step as ledgersStep #-}
    
    Previous
    Actions
    Next
    NewEpoch
    Made with Material for MkDocs