Ledger.BaseTypes

{-# OPTIONS --safe #-}

module Ledger.BaseTypes where

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


private


  Coin   = ℕ
  Slot   = ℕ
  Epoch  = ℕ


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