Basic Definitions for RefinedDiscrTree

Definitions

inductive Lean.Meta.RefinedDiscrTree.Key : Type

Discrimination tree key.

• star : Nat → Key

  A metavariable. This key matches with anything. It stores an index.

• opaque : Key

  An opaque variable. This key only matches with itself or Key.star.

• const : Name → Nat → Key

  A constant. It stores the name and the arity.

• fvar : FVarId → Nat → Key

  A free variable. It stores the FVarId and the arity.

• bvar : Nat → Nat → Key

  A bound variable, from a lambda or forall binder. It stores the De Bruijn index and the arity.

• lit : Literal → Key

  A literal.

• sort : Key

  A sort. Universe levels are ignored.

• lam : Key

  A lambda function.

• forall : Key

  A dependent arrow.

• proj : Name → Nat → Nat → Key

  A projection. It stores the structure name, the projection index and the arity.

instance Lean.Meta.RefinedDiscrTree.instInhabitedKey : Inhabited Key

instance Lean.Meta.RefinedDiscrTree.instBEqKey : BEq Key

instance Lean.Meta.RefinedDiscrTree.instReprKey : Repr Key

instance Lean.Meta.RefinedDiscrTree.instHashableKey : Hashable Key

def Lean.Meta.RefinedDiscrTree.Key.ctorIdx : Key → Nat

Constructor index used for ordering Key. Note that the index of the star pattern is 0, so that when looking up in a Trie, we can look at the start of the sorted array for all .star patterns.

instance Lean.Meta.RefinedDiscrTree.instLTKey : LT Key

instance Lean.Meta.RefinedDiscrTree.instDecidableLtKey (a b : Key) : Decidable (a < b)

instance Lean.Meta.RefinedDiscrTree.instToFormatKey : ToFormat Key

def Lean.Meta.RefinedDiscrTree.Key.arity : Key → Nat

Return the number of arguments that the Key takes.

inductive Lean.Meta.RefinedDiscrTree.Trie (α : Type) : Type

Discrimination tree trie. See RefinedDiscrTree.

• node {α : Type} (children : Array (Key × Trie α)) : Trie α

  Map from Key to Trie. Children is an Array of size at least 2, sorted in increasing order using Key.lt.

• path {α : Type} (keys : Array Key) (child : Trie α) : Trie α

  Sequence of nodes with only one child. keys is an Array of size at least 1.

• values {α : Type} (vs : Array α) : Trie α

  Leaf of the Trie. values is an Array of size at least 1.

instance Lean.Meta.RefinedDiscrTree.instInhabitedTrie {α : Type} : Inhabited (Trie α)

def Lean.Meta.RefinedDiscrTree.Trie.mkPath {α : Type} (keys : Array Key) (child : Trie α) : Trie α

Trie.path constructor that only inserts the path if it is non-empty.

def Lean.Meta.RefinedDiscrTree.Trie.singleton {α : Type} (keys : Array Key) (value : α) (i : Nat) : Trie α

Trie constructor for a single value, taking the keys starting at index i.

def Lean.Meta.RefinedDiscrTree.Trie.mkNode2 {α : Type} (k1 : Key) (t1 : Trie α) (k2 : Key) (t2 : Trie α) : Trie α

Trie.node constructor for combining two Key, Trie α pairs.

def Lean.Meta.RefinedDiscrTree.Trie.values! {α : Type} : Trie α → Array α

Return the values from a Trie α, assuming that it is a leaf

def Lean.Meta.RefinedDiscrTree.Trie.children! {α : Type} : Trie α → Array (Key × Trie α)

Return the children of a Trie α, assuming that it is not a leaf. The result is sorted by the Key's

instance Lean.Meta.RefinedDiscrTree.instToFormatTrie {α : Type} [ToFormat α] : ToFormat (Trie α)

structure Lean.Meta.RefinedDiscrTree (α : Type) : Type

Discrimination tree. It is an index from expressions to values of type α.

• root : PersistentHashMap Key (Trie α)

  The underlying PersistentHashMap of a RefinedDiscrTree.

instance Lean.Meta.RefinedDiscrTree.instInhabited {α : Type} : Inhabited (RefinedDiscrTree α)

instance Lean.Meta.RefinedDiscrTree.instToFormat {α : Type} [ToFormat α] : ToFormat (RefinedDiscrTree α)