logo
Formal Ledger Specification
Ledger.Dijkstra.Specification
Initializing search
    GitHub
    • Navigation
    • References
    GitHub
      • Home
      • Guide for Contributors
        • Notation
      • Ledger
        • Prelude
        • Introduction
        • Properties
          • Base
            • HSTypes
            • Util
          • HasCoin
          • Instances
          • Numeric
            • PositiveNat
            • UnitInterval
            • Address
            • Crypto
            • Epoch
        • Conway
          • Specification
            • Abstract
            • BlockBody
              • Properties
                • Computational
            • Certs
              • Properties
                • Computational
                • PoV
                • PoVLemmas
                • VoteDelegsVDeleg
            • Chain
              • Properties
                • Computational
                • CredDepsEqualDomRwds
                • EpochStep
                • GovDepsMatch
                • PParamsWellFormed
            • Enact
              • Properties
                • Computational
            • Epoch
              • Properties
                • Computational
                • ConstRwds
                • GovDepsMatch
                • NoPropSameDReps
            • Fees
            • Gov
              • Base
              • Actions
              • Properties
                • Computational
                • ChangePPGroup
            • Ledger.Ledger
              • Properties
                • Base
                • Computational
                • GovDepsMatch
                • PoV
            • PoolReap
            • PParams
            • Properties
            • Ratify
              • Properties
                • Computational
            • Rewards
            • RewardUpdate
              • Properties
                • Computational
            • Script
              • Base
              • Timelock
              • Validation
              • Base
              • Coin
              • ValueSet
              • ValueVector
            • Transaction
            • Utxo
              • Properties
                • Base
                • Computational
                • GenMinspend
                • MinSpend
                • PoV
            • Utxow
              • Properties
                • Computational
              • 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
        • Definitions
        • Agda Prelude
            • ComputationalRelation
            • HasSubset
            • HasSubtract
              • Instance
            • Hashable
            • STS
          • MyDebugOptions
    • References

    Ledger.Dijkstra.Specification

    {-# OPTIONS --safe #-}
    module Ledger.Dijkstra.Specification where
    
    import Ledger.Core.Specification.Address renaming (RwdAddr to RewardAddress)
    import Ledger.Core.Specification.Epoch
    
    import Ledger.Dijkstra.Specification.Certs
    import Ledger.Dijkstra.Specification.Gov.Base
    import Ledger.Dijkstra.Specification.Gov.Actions
    import Ledger.Dijkstra.Specification.PParams
    import Ledger.Dijkstra.Specification.Script
    import Ledger.Dijkstra.Specification.Script.Validation
    import Ledger.Dijkstra.Specification.TokenAlgebra.Base
    import Ledger.Dijkstra.Specification.Transaction
    
    Made with Material for MkDocs