max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix Util.Heartbeats module-doc (#3954)

Browse source
This commit is contained in:
Kim Morrison 2024-04-22 09:02:58 +02:00 • committed by GitHub
parent ea23ab6fef
commit 22ce2fea9b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Util/Heartbeats.lean
View file

@ -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