← Copula mathematical handbook

def Aesop.indexConfig : Lean.Meta.ConfigWithKey

The configuration used by all Aesop indices.

Equations

• Aesop.indexConfig = { transparency := Lean.Meta.TransparencyMode.reducible, proj := Lean.Meta.ProjReductionKind.no }.toConfigWithKey

def Aesop.mkDiscrTreePath (e : Lean.Expr) : Lean.MetaM (Array Lean.Meta.DiscrTree.Key)

Equations

• Aesop.mkDiscrTreePath e = Lean.Meta.withConfigWithKey Aesop.indexConfig (Lean.Meta.DiscrTree.mkPath e)

def Aesop.getUnify {α : Type} (t : Lean.Meta.DiscrTree α) (e : Lean.Expr) : Lean.MetaM (Array α)

Equations

• Aesop.getUnify t e = Lean.Meta.withConfigWithKey Aesop.indexConfig (t.getUnify e)

def Aesop.getMatch {α : Type} (t : Lean.Meta.DiscrTree α) (e : Lean.Expr) : Lean.MetaM (Array α)

Equations

• Aesop.getMatch t e = Lean.Meta.withConfigWithKey Aesop.indexConfig (t.getMatch e)