Formal Ledger Specification

Ledger

Formal Ledger Specification

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

Ledger

module Ledger where

import Ledger.PreConway
import Ledger.Conway