- map : Lean.PHashMap Lean.HeadIndex (Lean.AssocList Lean.Expr α)
A mapping that indentifies definitionally equal expressions.
We implement it as a mapping from HeadIndex to AssocList Expr α.
Remark: this map may be quite inefficient if there are many HeadIndex collisions.
Instances For
def
Lean.Meta.KExprMap.find?
{α : Type}
(m : Lean.Meta.KExprMap α)
(e : Lean.Expr)
:
Lean.MetaM (Option α)
Return some v if there is an entry e ↦ v in m.
Instances For
Insert e ↦ v into m