------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive System.Clock simple bindings to Haskell functions
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible #-}
module System.Clock.Primitive where
open import Agda.Builtin.Nat using (Nat)
open import IO.Primitive.Core using (IO)
open import Foreign.Haskell using (Pair)
data Clock : Set where
monotonic realTime processCPUTime : Clock
threadCPUTime monotonicRaw bootTime : Clock
monotonicCoarse realTimeCoarse : Clock
{-# COMPILE GHC Clock = data Clock (Monotonic | Realtime | ProcessCPUTime
| ThreadCPUTime | MonotonicRaw | Boottime
| MonotonicCoarse | RealtimeCoarse )
#-}
postulate getTime : Clock → IO (Pair Nat Nat)
{-# FOREIGN GHC import System.Clock #-}
{-# FOREIGN GHC import Data.Function #-}
{-# COMPILE GHC getTime = fmap (\ (TimeSpec a b) -> ((,) `on` fromIntegral) a b) . getTime #-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4