Documentation

Aesop.Stats.Basic

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

                Number of successful applications of a rule.

              • numFailed : Nat

                Number of failed applications of a rule.

              • elapsedSuccessful : Aesop.Nanos

                Total elapsed time of successful applications of a rule.

              • elapsedFailed : Aesop.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 :
                          Instances
                            Equations
                            • Aesop.instMonadLiftBaseIOOfMonadStats = { monadLift := fun {α : Type} => monadLift }
                            @[always_inline]
                            Equations
                            Instances For
                              @[always_inline]
                              Equations
                              Instances For
                                @[always_inline]
                                Equations
                                • Aesop.isStatsCollectionOrTracingEnabled = (Aesop.isStatsCollectionEnabled <||> Aesop.isStatsTracingEnabled)
                                Instances For
                                  @[always_inline]
                                  def Aesop.profiling {m : TypeType} [Monad m] [Aesop.MonadStats m] {α : Type} (recordStats : Aesop.StatsαAesop.NanosAesop.Stats) (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] [Aesop.MonadStats 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] [Aesop.MonadStats m] {α : Type} (rule : Aesop.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
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For