From 22ce2fea9b93b53a338114dde67c27e881aa1b24 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 22 Apr 2024 09:02:58 +0200 Subject: [PATCH] chore: fix Util.Heartbeats module-doc (#3954) --- src/Lean/Util/Heartbeats.lean | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/src/Lean/Util/Heartbeats.lean b/src/Lean/Util/Heartbeats.lean index fb972a37be..88cc3c2980 100644 --- a/src/Lean/Util/Heartbeats.lean +++ b/src/Lean/Util/Heartbeats.lean @@ -1,19 +1,15 @@ /- -Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Copyright (c) 2023 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Kim Morrison -/ prelude import Lean.CoreM /-! -# Lean.Heartbeats - -This provides some utilities is the first file in the Lean import hierarchy. It is responsible for setting -up basic definitions, most of which Lean already has "built in knowledge" about, -so it is important that they be set up in exactly this way. (For example, Lean will -use `PUnit` in the desugaring of `do` notation, or in the pattern match compiler.) +# Heartbeats +Functions for interacting with the deterministic timeout heartbeat mechanism. -/ namespace Lean