Documentation

Lean.Util.Heartbeats

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.)

def Lean.withHeartbeats {m : TypeType u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] (x : m α) :
m (α × Nat)

Counts the number of heartbeats used during a monadic function.

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.

Equations
Instances For

    Returns the current maxHeartbeats.

    Equations
    Instances For

      Returns the current initHeartbeats.

      Equations
      Instances For

        Returns the remaining heartbeats available in this computation.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Returns the percentage of the max heartbeats allowed that have been consumed so far in this computation.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Log a message if it looks like we ran out of time.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For