Skip to content

Commit

Permalink
chore: remove mention of Lean.withSeconds (#5481)
Browse files Browse the repository at this point in the history
There's a comment on `withHeartbeats` that says "See also
Lean.withSeconds", but his definition does not seem to actually exist.
Hence, I've removed the comment.
  • Loading branch information
alexkeizer authored Sep 26, 2024
1 parent 1fb75b6 commit 91a0334
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion src/Lean/Util/Heartbeats.lean
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@ Remember that user facing heartbeats (e.g. as used in `set_option maxHeartbeats`
differ from the internally tracked heartbeats by a factor of 1000,
so you need to divide the results here by 1000 before comparing with user facing numbers.
-/
-- See also `Lean.withSeconds`
def withHeartbeats [Monad m] [MonadLiftT BaseIO m] (x : m α) : m (α × Nat) := do
let start ← IO.getNumHeartbeats
let r ← x
Expand Down

0 comments on commit 91a0334

Please sign in to comment.