See file DiscrTree.lean for the actual implementation and documentation.

inductive Lean.Meta.DiscrTree.Key : Type

• const: Lean.Name → Nat → Lean.Meta.DiscrTree.Key
• fvar: Lean.FVarId → Nat → Lean.Meta.DiscrTree.Key
• lit: Lean.Literal → Lean.Meta.DiscrTree.Key
• star: Lean.Meta.DiscrTree.Key
• other: Lean.Meta.DiscrTree.Key
• arrow: Lean.Meta.DiscrTree.Key
• proj: Lean.Name → Nat → Lean.Meta.DiscrTree.Key

instance Lean.Meta.DiscrTree.instInhabitedKey : Inhabited Lean.Meta.DiscrTree.Key

Equations

• Lean.Meta.DiscrTree.instInhabitedKey = { default := Lean.Meta.DiscrTree.Key.const default default }

instance Lean.Meta.DiscrTree.instBEqKey : BEq Lean.Meta.DiscrTree.Key

Equations

• Lean.Meta.DiscrTree.instBEqKey = { beq := Lean.Meta.DiscrTree.beqKey✝ }

instance Lean.Meta.DiscrTree.instReprKey : Repr Lean.Meta.DiscrTree.Key

Equations

• Lean.Meta.DiscrTree.instReprKey = { reprPrec := Lean.Meta.DiscrTree.reprKey✝ }

def Lean.Meta.DiscrTree.Key.hash : Lean.Meta.DiscrTree.Key → UInt64

Equations

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

instance Lean.Meta.DiscrTree.instHashableKey : Hashable Lean.Meta.DiscrTree.Key

Equations

• Lean.Meta.DiscrTree.instHashableKey = { hash := Lean.Meta.DiscrTree.Key.hash }

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

• node: {α : Type} → Array α → Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Lean.Meta.DiscrTree.Trie α

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

• root : Lean.PersistentHashMap Lean.Meta.DiscrTree.Key (Lean.Meta.DiscrTree.Trie α)