structure WeightedNetKAT.Perf.Marker : Type

• name : Option String
• ns : ℕ

def WeightedNetKAT.Perf.mark (name : Option String := none) : IO Marker

Equations

• WeightedNetKAT.Perf.mark name = do let __do_lift ← liftM IO.monoNanosNow have m : WeightedNetKAT.Perf.Marker := { name := name, ns := __do_lift } pure m

structure WeightedNetKAT.Perf.Duration : Type

• ns : ℕ

@[implicit_reducible]

instance WeightedNetKAT.Perf.instToStringDuration : ToString Duration

Equations

• One or more equations did not get rendered due to their size.

def WeightedNetKAT.Perf.Marker.since (m : Marker) : IO Duration

Equations

• One or more equations did not get rendered due to their size.

def WeightedNetKAT.Perf.time {α : Type} (name : String) (f : Unit → α) : IO α

Equations

• WeightedNetKAT.Perf.time name f = do let m ← WeightedNetKAT.Perf.mark (some name) let v ← IO.lazyPure f let __discr ← m.since have x : WeightedNetKAT.Perf.Duration := __discr pure v

def WeightedNetKAT.Perf.timeIO {α : Type} (name : String) (f : Unit → IO α) : IO α

Equations

• WeightedNetKAT.Perf.timeIO name f = do let m ← WeightedNetKAT.Perf.mark (some name) let v ← f () let __discr ← m.since have x : WeightedNetKAT.Perf.Duration := __discr pure v