Documentation

Lean.Meta.DiscrTree

source
def Lean.Meta.DiscrTree.Key.ctorIdx:
Lean.Meta.DiscrTree.Key → Nat
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.DiscrTree.Key.lt:
Lean.Meta.DiscrTree.Key → Lean.Meta.DiscrTree.Key → Bool
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Meta.DiscrTree.instLTKey:
LT Lean.Meta.DiscrTree.Key
Equations
source
instance Lean.Meta.DiscrTree.instDecidableLtKeyInstLTKey (a : Lean.Meta.DiscrTree.Key) (b : Lean.Meta.DiscrTree.Key) :
Decidable (a < b)
Equations
source
def Lean.Meta.DiscrTree.Key.format:
Lean.Meta.DiscrTree.Key → Lean.Format
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Meta.DiscrTree.instToFormatKey:
Lean.ToFormat Lean.Meta.DiscrTree.Key
Equations
source
def Lean.Meta.DiscrTree.Key.arity:
Lean.Meta.DiscrTree.Key → Nat
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Meta.DiscrTree.instInhabitedTrie {α : Type} :
Inhabited (Lean.Meta.DiscrTree.Trie α)
Equations
source
def Lean.Meta.DiscrTree.empty {α : Type} :
Lean.Meta.DiscrTree α
Equations
source
partial def Lean.Meta.DiscrTree.Trie.format {α : Type} [inst : Lean.ToFormat α] :
Lean.Meta.DiscrTree.Trie α → Lean.Format
source
instance Lean.Meta.DiscrTree.instToFormatTrie {α : Type} [inst : Lean.ToFormat α] :
Lean.ToFormat (Lean.Meta.DiscrTree.Trie α)
Equations
  • Lean.Meta.DiscrTree.instToFormatTrie = { format := Lean.Meta.DiscrTree.Trie.format }
source
def Lean.Meta.DiscrTree.format {α : Type} [inst : Lean.ToFormat α] (d : Lean.Meta.DiscrTree α) :
Lean.Format
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Meta.DiscrTree.instToFormatDiscrTree {α : Type} [inst : Lean.ToFormat α] :
Lean.ToFormat (Lean.Meta.DiscrTree α)
Equations
  • Lean.Meta.DiscrTree.instToFormatDiscrTree = { format := Lean.Meta.DiscrTree.format }
source
instance Lean.Meta.DiscrTree.instInhabitedDiscrTree {α : Type} :
Inhabited (Lean.Meta.DiscrTree α)
Equations
source
def Lean.Meta.DiscrTree.mkNoindexAnnotation (e : Lean.Expr) :
Lean.Expr
Equations
source
def Lean.Meta.DiscrTree.hasNoindexAnnotation (e : Lean.Expr) :
Bool
Equations
source
def Lean.Meta.DiscrTree.whnfDT (e : Lean.Expr) (root : Bool) :
Lean.MetaM Lean.Expr

whnf for the discrimination tree module

Equations
source
partial def Lean.Meta.DiscrTree.mkPathAux (root : Bool) (todo : Array Lean.Expr) (keys : Array Lean.Meta.DiscrTree.Key) :
Lean.MetaM (Array Lean.Meta.DiscrTree.Key)
source
def Lean.Meta.DiscrTree.mkPath (e : Lean.Expr) :
Lean.MetaM (Array Lean.Meta.DiscrTree.Key)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.DiscrTree.insertCore {α : Type} [inst : BEq α] (d : Lean.Meta.DiscrTree α) (keys : Array Lean.Meta.DiscrTree.Key) (v : α) :
Lean.Meta.DiscrTree α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.DiscrTree.insert {α : Type} [inst : BEq α] (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) (v : α) :
Lean.MetaM (Lean.Meta.DiscrTree α)
Equations
source
def Lean.Meta.DiscrTree.getMatch {α : Type} (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) :
Lean.MetaM (Array α)

Find values that match e in d.

Equations
source
def Lean.Meta.DiscrTree.getMatchWithExtra {α : Type} (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) :
Lean.MetaM (Array (α × Nat))

Similar to getMatch, but returns solutions that are prefixes of e. We store the number of ignored arguments in the result.

Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.DiscrTree.getMatchWithExtra.mayMatchPrefix {α : Type} (d : Lean.Meta.DiscrTree α) (k : Lean.Meta.DiscrTree.Key) :
Lean.MetaM Bool
source
partial def Lean.Meta.DiscrTree.getMatchWithExtra.go {α : Type} (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) (numExtra : Nat) (result : Array (α × Nat)) :
Lean.MetaM (Array (α × Nat))
source
def Lean.Meta.DiscrTree.getUnify {α : Type} (d : Lean.Meta.DiscrTree α) (e : Lean.Expr) :
Lean.MetaM (Array α)
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.DiscrTree.getUnify.process {α : Type} (skip : Nat) (todo : Array Lean.Expr) (c : Lean.Meta.DiscrTree.Trie α) (result : Array α) :
Lean.MetaM (Array α)