logo
Formal Ledger Specification
Foreign
Initializing search
    GitHub
    • Home
    • Preliminaries
    • Core
    • Conway
    • Dijkstra
    • Appendix
    GitHub
    • Home
      • Introduction
      • Notation
      • Earlier Eras
      • Introduction
        • Address
        • Crypto
        • Epoch
        • ProtocolVersion
      • Introduction
        • Abstract
        • BlockBody
          • Properties
            • Computational
        • Certs
          • Properties
            • Computational
            • PoV
            • PoVLemmas
            • VoteDelegsVDeleg
        • Chain
          • Properties
            • Computational
            • CredDepsEqualDomRwds
            • EpochStep
            • GovDepsMatch
            • PParamsWellFormed
        • Enact
          • Properties
            • Computational
        • Epoch
          • Properties
            • Computational
            • ConstRwds
            • ExpiredDReps
            • GovDepsMatch
            • NoPropSameDReps
        • Fees
        • Gov
          • Base
          • Actions
          • Properties
            • Computational
            • ChangePPGroup
        • Ledger
          • Properties
            • Base
            • Computational
            • GovDepsMatch
            • PoV
        • PoolReap
            • Computational
        • PParams
        • Properties
        • Ratify
          • Properties
            • Computational
        • Rewards
          • Properties
            • Computational
        • RewardUpdate
          • Properties
            • Computational
        • Script
          • Base
          • ScriptPurpose
          • Timelock
          • Validation
          • Base
          • Coin
          • ValueSet
          • ValueVector
        • Transaction
        • Utxo
          • Properties
            • Base
            • Computational
            • GenMinspend
            • MinSpend
            • PoV
        • Utxow
          • Properties
            • Computational
          • GovStructure
      • Introduction
      • Abstract
      • BlockBody
        • Properties
          • Computational
      • Certs
        • Properties
          • Computational
      • Chain
        • Properties
          • Computational
      • Enact
        • Properties
          • Computational
      • Epoch
        • Properties
          • Computational
      • Fees
      • Gov
        • Actions
        • Base
        • Properties
          • Computational
      • Ledger
        • Properties
          • Computational
      • PoolReap
        • Properties
          • Computational
      • PParams
      • Ratify
        • Properties
          • Computational
      • Rewards
        • Properties
          • Computational
      • RewardUpdate
        • Properties
          • Computational
      • Script
        • Base
        • ScriptPurpose
        • Validation
      • TokenAlgebra
      • Transaction
      • Utxo
        • Properties
          • Computational
      • Utxow
        • Properties
          • Computational
        • Definitions
        • Essential Agda
          • Bootstrapping Governance
          • Bootstrapping EnactState
        • Prelude
        • Ledger
        • Ledger.Core
          • Foreign
            • Address
            • Crypto
              • Base
              • Structure
            • Epoch
            • ExternalFunctions
        • Ledger.Prelude
          • Base
            • HSTypes
            • Util
          • HasCoin
          • Instances
          • Numeric
            • PositiveNat
            • UnitInterval
          • STS
          • ComputationalRelation
          • TypeClasses
            • TypeClasses
            • HasSubset
            • HasSubtract
              • Instance
          • Convertible
            • Deriving
            • DerivingTest
          • HaskellTypes
            • Deriving
        • MyDebugOptions
          • Examples
            • HelloWorld
            • SucceedIfNumber
              • Datum
                • Cleanup
                • Close
                • Deposit
                • Lib
                • OffChain
                • Open
                • Start
                • Transfer
                • Withdraw
                • Trace
              • Validator
              • Datum
                • Close
                • Exchange
                • Lib
                • OffChain
                • Start
                • Update
                • Trace
              • Validator
              • Datum
                • AddSig
                • Lib
                • OffChain
                • Open
                • Pay
                • Propose
                • Trace
              • Validator
              • Datum
                • AddSig
                • Cancel
                • Cleanup
                • Lib
                • OffChain
                • Open
                • Pay
                • Propose
                • Trace
              • Validator
          • AbstractImplementation
          • LedgerImplementation
          • Lib
          • Prelude
          • SymbolicData
          • Ledger.Dijkstra
          • Ledger.PreConway
              • NewPP
                • Properties
              • PPUp
                • Properties
            • NewPP
              • Properties
            • PPUp
              • Properties
          • Ledger.Conway
            • Foreign
              • HSStructures
              • Cert
              • Certs
              • Chain
              • Enact
              • Epoch
              • ExternalStructures
              • Gov
                • Core
                • Actions
              • Ledger
              • NewEpoch
              • PParams
              • Ratify
              • Rewards
              • Transaction
              • Script
                • Base
                • Structure
              • Utxo
          • Conformance
            • Certs
              • Properties
            • Epoch
              • Properties
            • Equivalence
              • Bisimilarity
              • Certs
              • Convert
              • Deposits
              • Map
              • Utxo
            • Gov
            • Ledger
              • Properties
            • Properties
            • Rewards
            • Utxo
              • Properties
            • Utxow
              • Properties

    Foreign

    module Ledger.Conway.Foreign where
    
    open import Ledger.Conway.Foreign.Cert public
    open import Ledger.Conway.Foreign.Chain public
    open import Ledger.Conway.Foreign.Certs public
    open import Ledger.Conway.Foreign.Enact public
    open import Ledger.Conway.Foreign.Epoch public
    open import Ledger.Conway.Foreign.Gov public
    open import Ledger.Conway.Foreign.Ledger public
    open import Ledger.Conway.Foreign.NewEpoch public
    open import Ledger.Conway.Foreign.Ratify public
    open import Ledger.Conway.Foreign.Utxo public
    open import Ledger.Conway.Foreign.Script public
    
    Previous
    Ledger.Conway
    Next
    HSStructures
    Made with Material for MkDocs