logo
Formal Ledger Specification
Ledger
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
        • Account
        • BlockBody
          • Properties
            • Computational
        • Certs
          • Properties
            • Computational
        • Chain
          • Properties
            • Computational
        • Enact
          • Properties
            • Computational
        • Entities
          • 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
          • Native
          • ScriptPurpose
          • Validation
        • TokenAlgebra
        • Transaction
        • Utxo
          • Properties
            • Computational
        • Utxow
          • Properties
            • Computational
        • Definitions
        • Essential Agda
          • Bootstrapping Governance
          • Bootstrapping EnactState
        • Prelude
        • Ledger
        • Ledger.Core
        • Ledger.Prelude
          • Base
            • HSTypes
            • Util
          • HasCoin
          • Instances
          • Numeric
            • PositiveNat
            • UnitInterval
          • STS
          • ComputationalRelation
          • TypeClasses
            • TypeClasses
            • HasSubset
            • HasSubtract
              • Instance
        • MyDebugOptions
          • Ledger.Dijkstra
          • Ledger.PreConway
              • NewPP
                • Properties
              • PPUp
                • Properties
            • NewPP
              • Properties
            • PPUp
              • Properties
          • Ledger.Conway
          • Conformance
            • Certs
              • Properties
            • Epoch
              • Properties
            • Equivalence
              • Bisimilarity
              • Certs
              • Convert
              • Deposits
              • Utxo
            • Gov
            • Ledger
              • Properties
            • Properties
            • Rewards
            • Utxo
              • Properties
            • Utxow
              • Properties

    Ledger

    module Ledger where
    
    import Ledger.Introduction
    import Ledger.PreConway
    import Ledger.Core
    import Ledger.Conway
    import Ledger.Dijkstra
    
    import EssentialAgda
    
    Previous
    Prelude
    Next
    Ledger.Core
    Made with Material for MkDocs