Documentation

Aesop.Stats.Basic

Equations
Equations
  • One or more equations did not get rendered due to their size.
structure Aesop.Stats :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • numSuccessful : Nat

    Number of successful applications of a rule.

  • numFailed : Nat

    Number of failed applications of a rule.

  • elapsedSuccessful : Nanos

    Total elapsed time of successful applications of a rule.

  • elapsedFailed : Nanos

    Total elapsed time of failed applications of a rule.

Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
Equations
class Aesop.MonadStats (m : TypeType) extends Lean.MonadOptions m :
Instances
    @[always_inline]
    def Aesop.profiling {m : TypeType} [Monad m] [MonadStats m] {α : Type} (recordStats : StatsαNanosStats) (x : m α) :
    m α
    Equations
    • One or more equations did not get rendered due to their size.
    @[always_inline]
    def Aesop.profilingRuleSelection {m : TypeType} [Monad m] [MonadStats m] {α : Type} :
    m αm α
    Equations
    • One or more equations did not get rendered due to their size.
    @[always_inline]
    def Aesop.profilingRule {m : TypeType} [Monad m] [MonadStats m] {α : Type} (rule : DisplayRuleName) (wasSuccessful : αBool) :
    m αm α
    Equations
    • One or more equations did not get rendered due to their size.
    def Aesop.modifyCurrentStats {m : TypeType} [Monad m] [MonadStats m] (f : StatsStats) :
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.