Documentation

Aesop.Stats.Basic

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      Instances For
        structure Aesop.Stats :
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            Instances For
              • 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.

              Instances For
                Equations
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[reducible, inline]
                        Equations
                        Instances For
                          class Aesop.MonadStats (m : TypeType) extends Lean.MonadOptions m :
                          Instances
                            instance Aesop.instMonadStatsStateRefT' {m : TypeType} {ω σ : Type} [MonadStats m] :
                            Equations
                            • One or more equations did not get rendered due to their size.
                            instance Aesop.instMonadStatsReaderT {m : TypeType} {α : Type} [MonadStats m] :
                            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.
                            @[always_inline]
                            def Aesop.profiling {m : TypeType} [Monad m] [MonadStats m] [MonadLiftT BaseIO m] {α : Type} (recordStats : StatsαNanosStats) (x : m α) :
                            m α
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[always_inline]
                              def Aesop.profilingRuleSelection {m : TypeType} [Monad m] [MonadStats m] [MonadLiftT BaseIO m] {α : Type} :
                              m αm α
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[always_inline]
                                def Aesop.profilingRule {m : TypeType} [Monad m] [MonadStats m] [MonadLiftT BaseIO m] {α : Type} (rule : DisplayRuleName) (wasSuccessful : αBool) :
                                m αm α
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For