Documentation

Aesop.Index.DiscrTreeConfig

source
def Aesop.indexConfig :
Lean.Meta.ConfigWithKey

The configuration used by all Aesop indices.

Equations
    Instances For
      source
      def Aesop.mkDiscrTreePath (e : Lean.Expr) :
      Lean.MetaM (Array Lean.Meta.DiscrTree.Key)
      Equations
        Instances For
          source
          def Aesop.getUnify {α : Type} (t : Lean.Meta.DiscrTree α) (e : Lean.Expr) :
          Lean.MetaM (Array α)
          Equations
            Instances For
              source
              def Aesop.getMatch {α : Type} (t : Lean.Meta.DiscrTree α) (e : Lean.Expr) :
              Lean.MetaM (Array α)
              Equations
                Instances For