Base Types

This section is part of the Ledger.Conway.BaseTypes module of the formal ledger specification, in which we define some of the most basic types used throughout the ledger.

{-# OPTIONS --safe #-}

module Ledger.Conway.BaseTypes where

open import Agda.Builtin.FromNat
open import Prelude using (ℕ; _×_)
open import Data.Rational using (ℚ; _≤_)
open import Data.Refinement using (Refinement-syntax)

private

Some basic types used in many places in the ledger

  Coin   = ℕ
  Slot   = ℕ
  Epoch  = ℕ

Refinement types used in some places in the ledger

  UnitInterval = [ x ∈ ℚ ∣ ( ≤ x) × (x ≤ ) ]