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

    Epoch

    module Ledger.Conway.Foreign.HSLedger.Epoch where
    
    open import Ledger.Conway.Foreign.HSLedger.BaseTypes
    open import Ledger.Conway.Foreign.HSLedger.Enact
    open import Ledger.Conway.Foreign.HSLedger.Ledger
    open import Ledger.Conway.Foreign.HSLedger.PParams
    open import Ledger.Conway.Foreign.HSLedger.Ratify
    open import Ledger.Conway.Foreign.HSLedger.Rewards
    
    open import Ledger.Conway.Conformance.Epoch it it
    open import Ledger.Conway.Conformance.Epoch.Properties it it
    
    instance
      HsTy-EpochState = autoHsType EpochState ⊣ withConstructor "MkEpochState"
                                              • fieldPrefix "es"
      Conv-EpochState = autoConvert EpochState
    
    epoch-step : HsType (⊤ → EpochState → Epoch → ComputationResult ⊥ EpochState)
    epoch-step = to (compute Computational-EPOCH)
    
    {-# COMPILE GHC epoch-step as epochStep #-}
    
    Previous
    Enact
    Next
    ExternalStructures
    Made with Material for MkDocs