structure Aesop.EMap (α : Type u_1) : Type u_1

A map whose keys are expressions. Keys are identified up to defeq. We use reducible transparency and treat metavariables as rigid (i.e., unassignable).

• rep : Lean.PArray (Option (Lean.Expr × α))

  The mappings stored in the map. Defeq expressions are identified, so for each equivalence class of defeq expressions we only store one representative. Missing values indicate expressions that were removed from the map.

• idx : Lean.Meta.DiscrTree Nat

  An index for rep. For each expression e at index i in rep, idx.getMatch returns a list of indexes containing i. This is used as a pre-filter during lookups/insertions/modifications to reduce the number of defeq comparisons.

def Aesop.instInhabitedEMap.default {a✝ : Type u_1} : EMap a✝

@[implicit_reducible]

instance Aesop.instInhabitedEMap {a✝ : Type u_1} : Inhabited (EMap a✝)

def Aesop.EMap.empty {α : Type u_1} : EMap α

@[implicit_reducible]

instance Aesop.EMap.instEmptyCollection {α : Type u_1} : EmptyCollection (EMap α)

@[implicit_reducible]

instance Aesop.EMap.instForMProdExpr {m : Type → Type u_1} [Monad m] {α : Type u_2} : ForM m (EMap α) (Lean.Expr × α)

@[implicit_reducible]

instance Aesop.EMap.instForInProdExpr {m : Type → Type u_1} [Monad m] {α : Type u_2} : ForIn m (EMap α) (Lean.Expr × α)

def Aesop.EMap.foldlM {m : Type → Type u_1} [Monad m] {σ : Type} {α : Type u_2} (init : σ) (f : σ → Lean.Expr → α → m σ) (map : EMap α) : m σ

def Aesop.EMap.foldl {σ : Type} {α : Type u_1} (init : σ) (f : σ → Lean.Expr → α → σ) (map : EMap α) : σ

@[specialize #[]]

def Aesop.EMap.alterM {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] {α β : Type} (e : Lean.Expr) (f : α → m (Option α × β)) (map : EMap α) : m (EMap α × Option β)

def Aesop.EMap.alter {α β : Type} (e : Lean.Expr) (f : α → Option α × β) (map : EMap α) : Lean.MetaM (EMap α × Option β)

@[specialize #[]]

def Aesop.EMap.insertNew {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] {α : Type} (e : Lean.Expr) (a : α) (map : EMap α) : m (EMap α)

@[specialize #[]]

def Aesop.EMap.insertWithM {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] {α : Type} (e : Lean.Expr) (f : Option α → m α) (map : EMap α) : m (EMap α × Option α × α)

def Aesop.EMap.insertWith {α : Type} (e : Lean.Expr) (f : Option α → α) (map : EMap α) : Lean.MetaM (EMap α × Option α × α)

def Aesop.EMap.insert {α : Type} (e : Lean.Expr) (a : α) (map : EMap α) : Lean.MetaM (EMap α)

def Aesop.EMap.singleton {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] {α : Type} (e : Lean.Expr) (a : α) : m (EMap α)

def Aesop.EMap.findWithKey? {α : Type} (e : Lean.Expr) (map : EMap α) : Lean.MetaM (Option (Lean.Expr × α))

def Aesop.EMap.find? {α : Type} (e : Lean.Expr) (map : EMap α) : Lean.MetaM (Option α)

@[specialize #[]]

def Aesop.EMap.mapM {m : Type → Type u_1} [Monad m] {α β : Type} (f : Lean.Expr → α → m β) (map : EMap α) : m (EMap β)

def Aesop.EMap.map {α β : Type} (f : Lean.Expr → α → β) (map : EMap α) : EMap β