Documentation

Lean.Meta.DiscrTree

Equations
Equations
Equations
Equations
  • Lean.Meta.DiscrTree.instToFormatTrie = { format := Lean.Meta.DiscrTree.Trie.format }
Equations
Equations
  • Lean.Meta.DiscrTree.instToFormatDiscrTree = { format := Lean.Meta.DiscrTree.format }
Equations
def Lean.Meta.DiscrTree.insertCore {α : Type} [inst : BEq α] (d : Lean.Meta.DiscrTree α) (keys : Array Lean.Meta.DiscrTree.Key) (v : α) :
Equations
Equations
Equations
partial def Lean.Meta.DiscrTree.getMatchWithExtra.process {α : Type} (d : Lean.Meta.DiscrTree α) (k : Lean.Meta.DiscrTree.Key) (args : Subarray Lean.Expr) (numExtraArgs : Nat) (result : Array (α × Nat)) :
Equations
partial def Lean.Meta.DiscrTree.getUnify.process {α : Type} (skip : Nat) (todo : Array Lean.Expr) (c : Lean.Meta.DiscrTree.Trie α) (result : Array α) :