Documentation

Aesop.Index.DiscrTreeConfig

source
def Aesop.indexConfig :
Lean.Meta.ConfigWithKey

The configuration used by all Aesop indices.

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