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✝

Equations

• Aesop.instInhabitedEMap.default = { rep := default, idx := default }

@[implicit_reducible]

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

Equations

• Aesop.instInhabitedEMap = { default := Aesop.instInhabitedEMap.default }

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

Equations

• Aesop.EMap.empty = { rep := Lean.PersistentArray.empty, idx := Lean.Meta.DiscrTree.empty }

@[implicit_reducible]

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

Equations

• Aesop.EMap.instEmptyCollection = { emptyCollection := Aesop.EMap.empty }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

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

Equations

• Aesop.EMap.foldl init f map = inline (Aesop.EMap.foldlM init f map)

@[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 β)

Equations

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

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

Equations

• Aesop.EMap.alter e f map = inline (Aesop.EMap.alterM e (fun (a : α) => pure (f a)) map)

@[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 α)

Equations

• Aesop.EMap.insertNew e a map = do let idx ← liftM (map.idx.insert e map.rep.size) pure { rep := Lean.PersistentArray.push map.rep (some (e, a)), idx := idx }

@[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 α × α)

Equations

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

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

Equations

• Aesop.EMap.insertWith e f map = inline (Aesop.EMap.insertWithM e (fun (a? : Option α) => pure (f a?)) map)

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

Equations

• Aesop.EMap.insert e a map = (fun (x : Aesop.EMap α × Option α × α) => x.fst) <$> inline (Aesop.EMap.insertWithM e (fun (x : Option α) => pure a) map)

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

Equations

• Aesop.EMap.singleton e a = Aesop.EMap.insertNew e a Aesop.EMap.empty

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

Equations

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

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

Equations

• Aesop.EMap.find? e map = do let __do_lift ← inline (Aesop.EMap.findWithKey? e map) pure (Option.map (fun (x : Lean.Expr × α) => x.snd) __do_lift)

@[specialize #[]]

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

Equations

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

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

Equations

• Aesop.EMap.map f map = Aesop.EMap.mapM f map