def Lean.Meta.DiscrTree.mkNoindexAnnotation (e : Expr) : Expr

def Lean.Meta.DiscrTree.hasNoindexAnnotation (e : Expr) : Bool

@[implicit_reducible]

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

@[implicit_reducible]

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

def Lean.Meta.DiscrTree.empty {α : Type} : DiscrTree α

@[implicit_reducible]

instance Lean.Meta.DiscrTree.instToExprKey : ToExpr Key

def Lean.Meta.DiscrTree.Key.lt : Key → Key → Bool

@[implicit_reducible]

instance Lean.Meta.DiscrTree.instLTKey : LT Key

@[implicit_reducible]

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

def Lean.Meta.DiscrTree.Key.format : Key → Format

@[implicit_reducible]

instance Lean.Meta.DiscrTree.instToFormatKey : ToFormat Key

partial def Lean.Meta.DiscrTree.Trie.format {α : Type} [ToFormat α] : Trie α → Format

@[implicit_reducible]

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

def Lean.Meta.DiscrTree.format {α : Type} [ToFormat α] (d : DiscrTree α) : Format

@[implicit_reducible]

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

def Lean.Meta.DiscrTree.keysAsPattern (keys : Array Key) : CoreM MessageData

Helper function for converting an entry (i.e., Array Key) to the discrimination tree into MessageData that is more user-friendly. We use this function to implement diagnostic information.

def Lean.Meta.DiscrTree.insertKeyValue {α : Type} [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α

@[deprecated Lean.Meta.DiscrTree.insertKeyValue (since := "2026-01-02")]

def Lean.Meta.DiscrTree.insertCore {α : Type} [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α