Additions to Lean.Meta.DiscrTree #
def
Lean.Meta.DiscrTree.insertIfSpecific
{α : Type}
{s : Bool}
[BEq α]
(d : Lean.Meta.DiscrTree α s)
(keys : Array (Lean.Meta.DiscrTree.Key s))
(v : α)
:
Inserts a new key into a discrimination tree,
but only if it is not of the form #[*] or #[=, *, *, *].
Equations
- One or more equations did not get rendered due to their size.
Instances For
partial def
Lean.Meta.DiscrTree.getSubexpressionMatches
{α : Type}
{s : Bool}
(d : Lean.Meta.DiscrTree α s)
(e : Lean.Expr)
:
Lean.MetaM (Array α)
Find keys which match the expression, or some subexpression.
Note that repeated subexpressions will be visited each time they appear, making this operation potentially very expensive. It would be good to solve this problem!
Implementation: we reverse the results from getMatch,
so that we return lemmas matching larger subexpressions first,
and amongst those we return more specific lemmas first.
partial def
Lean.Meta.DiscrTree.Trie.mapArraysM
{m : Type → Type}
[Monad m]
{α : Type}
{s : Bool}
{β : Type}
(t : Lean.Meta.DiscrTree.Trie α s)
(f : Array α → m (Array β))
:
m (Lean.Meta.DiscrTree.Trie β s)
Apply a monadic function to the array of values at each node in a DiscrTree.
def
Lean.Meta.DiscrTree.mapArraysM
{m : Type → Type}
[Monad m]
{α : Type}
{s : Bool}
{β : Type}
(d : Lean.Meta.DiscrTree α s)
(f : Array α → m (Array β))
:
m (Lean.Meta.DiscrTree β s)
Apply a monadic function to the array of values at each node in a DiscrTree.
Equations
- Lean.Meta.DiscrTree.mapArraysM d f = do let __do_lift ← Lean.PersistentHashMap.mapM d.root fun t => Lean.Meta.DiscrTree.Trie.mapArraysM t f pure { root := __do_lift }
Instances For
def
Lean.Meta.DiscrTree.mapArrays
{α : Type}
{s : Bool}
{β : Type}
(d : Lean.Meta.DiscrTree α s)
(f : Array α → Array β)
:
Apply a function to the array of values at each node in a DiscrTree.
Equations
- Lean.Meta.DiscrTree.mapArrays d f = Lean.Meta.DiscrTree.mapArraysM d fun A => pure (f A)