Documentation

Aesop.Index

structure Aesop.Index (α : Type) :
Instances For
    Equations
    • Aesop.instInhabitedIndex = { default := { byTarget := default, byHyp := default, unindexed := default } }
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        def Aesop.Index.merge {α : Type} (ri₁ : Aesop.Index α) (ri₂ : Aesop.Index α) :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[specialize #[]]
          partial def Aesop.Index.add {α : Type} (r : Aesop.Rule α) (imode : Aesop.IndexingMode) (ri : Aesop.Index α) :
          def Aesop.Index.unindex {α : Type} (ri : Aesop.Index α) (p : Aesop.Rule αBool) :
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[always_inline]
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Aesop.Index.foldM {α : Type} {m : Type u_1 → Type u_1} {σ : Type u_1} [Monad m] (ri : Aesop.Index α) (f : σAesop.Rule αm σ) (init : σ) :
              m σ
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[inline]
                def Aesop.Index.fold {α : Type} {σ : Type u_1} (ri : Aesop.Index α) (f : σAesop.Rule ασ) (init : σ) :
                σ
                Equations
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[specialize #[]]
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[inline]
                      def Aesop.Index.applicableRules.insertIndexMatchResults {α : Type} [Ord α] (m : Lean.RBMap (Aesop.Rule α) (Array Aesop.IndexMatchLocation) Aesop.Rule.compareByPriorityThenName) (rs : Array (Aesop.Rule α × Array Aesop.IndexMatchLocation)) :
                      Lean.RBMap (Aesop.Rule α) (Array Aesop.IndexMatchLocation) Aesop.Rule.compareByPriorityThenName
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For