Documentation

Aesop.Stats.Basic

Instances For
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    structure Aesop.Stats :
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • Aesop.Stats.empty = { total := 0, configParsing := 0, ruleSetConstruction := 0, search := 0, ruleSelection := 0, ruleStats := #[] }
      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
                  @[inline, reducible]
                  Equations
                  Instances For
                    Instances
                      @[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