From 91a033488c28f62f94ae7230a319c9f86cbc474a Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Thu, 26 Sep 2024 13:15:58 -0500 Subject: [PATCH] chore: remove mention of `Lean.withSeconds` (#5481) 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. --- src/Lean/Util/Heartbeats.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Lean/Util/Heartbeats.lean b/src/Lean/Util/Heartbeats.lean index 88cc3c29807b..a6b0a48a6c4a 100644 --- a/src/Lean/Util/Heartbeats.lean +++ b/src/Lean/Util/Heartbeats.lean @@ -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