We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent ea01174 commit 4072e19Copy full SHA for 4072e19
1 file changed
Mathlib/Util/SleepHeartbeats.lean
@@ -30,8 +30,10 @@ def sleepAtLeastHeartbeats (n : Nat) : IO Unit := do
30
elab "sleep_heartbeats " n:num : tactic => do
31
match Syntax.isNatLit? n with
32
| none => throwIllFormedSyntax
33
- /- as this is a user facing command we multiply the user input by 1000 to match the maxHeartbeats
34
- option -/
+ /-
+ We multiply by `1000` to convert the user-facing heartbeat count to the
35
+ internal heartbeat counter used by `IO.getNumHeartbeats`.
36
+ -/
37
| some m => sleepAtLeastHeartbeats (m * 1000)
38
39
example : 1 = 1 := by
0 commit comments