Documentation

Lean.Meta.KExprMap

structure Lean.Meta.KExprMap (α : Type) :

Type

map : Std.PHashMap Lean.HeadIndex (Std.AssocList Lean.Expr α)

A mapping that indentifies definitionally equal expressions. We implement it as a mapping from HeadIndex to Std.AssocList Expr α.

Remark: this map may be quite inefficient if there are many HeadIndex collisions.

instance Lean.Meta.instInhabitedKExprMap:

{a : Type} → Inhabited (Lean.Meta.KExprMap a)

Equations

Lean.Meta.instInhabitedKExprMap = { default := { map := default } }

def Lean.Meta.KExprMap.find? {α : Type} (m : Lean.Meta.KExprMap α) (e : Lean.Expr) :

Lean.MetaM (Option α)

Equations

One or more equations did not get rendered due to their size.

def Lean.Meta.KExprMap.insert {α : Type} (m : Lean.Meta.KExprMap α) (e : Lean.Expr) (v : α) :

Lean.MetaM (Lean.Meta.KExprMap α)

Equations

One or more equations did not get rendered due to their size.