record Timed : Type -> Type- Totality: total
Visibility: public export
Constructor: MkTimed : a -> String -> Nat -> Clock Duration -> Clock Duration -> Timed a
Projections:
.description : Timed a -> String.result : Timed a -> a.runs : Timed a -> Nat.time : Timed a -> Clock Duration.totalTime : Timed a -> Clock Duration
Hint: Show (Timed a)
.result : Timed a -> a- Visibility: public export
result : Timed a -> a- Visibility: public export
.description : Timed a -> String- Visibility: public export
description : Timed a -> String- Visibility: public export
.runs : Timed a -> Nat- Visibility: public export
runs : Timed a -> Nat- Visibility: public export
.totalTime : Timed a -> Clock Duration- Visibility: public export
totalTime : Timed a -> Clock Duration- Visibility: public export
.time : Timed a -> Clock Duration- Visibility: public export
time : Timed a -> Clock Duration- Visibility: public export
timeIO : String -> IO a -> IO (Timed a) Time an `IO` action
Visibility: exportdefaultTime : Clock Duration Default duration of each benchmark
Visibility: public exportbenchIO : {default defaultTime _ : Clock Duration} -> String -> IO a -> IO (Timed a) Benchmark an IO operation.
This runs the given action repeatedly, until the target time has been reached.
Visibility: exportbench : {default defaultTime _ : Clock Duration} -> String -> (a -> b) -> a -> IO (Timed b) Benchmark a function with a given input.
This runs the function repeatedly until enough time has passed.
The default time to benchmark is 1 second, but this can be changed
with `targetTime`.
Visibility: export