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

Equations

• Lean.Meta.DiscrTree.mkNoindexAnnotation e = Lean.mkAnnotation `noindex e

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

Equations

• Lean.Meta.DiscrTree.hasNoindexAnnotation e = (Lean.annotation? `noindex e).isSome

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

Equations

• Lean.Meta.DiscrTree.instInhabitedTrie = { default := Lean.Meta.DiscrTree.Trie.node #[] #[] }

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

Equations

• Lean.Meta.DiscrTree.instInhabited = { default := { } }

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

Equations

• Lean.Meta.DiscrTree.empty = { }

instance Lean.Meta.DiscrTree.instToExprKey : ToExpr Key

Equations

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

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

Equations

• (Lean.Meta.DiscrTree.Key.lit v₁).lt (Lean.Meta.DiscrTree.Key.lit v₂) = decide (v₁ < v₂)
• (Lean.Meta.DiscrTree.Key.fvar n₁ a₁).lt (Lean.Meta.DiscrTree.Key.fvar n₂ a₂) = (n₁.name.quickLt n₂.name || n₁ == n₂ && decide (a₁ < a₂))
• (Lean.Meta.DiscrTree.Key.const n₁ a₁).lt (Lean.Meta.DiscrTree.Key.const n₂ a₂) = (n₁.quickLt n₂ || n₁ == n₂ && decide (a₁ < a₂))
• (Lean.Meta.DiscrTree.Key.proj s₁ i₁ a₁).lt (Lean.Meta.DiscrTree.Key.proj s₂ i₂ a₂) = (s₁.quickLt s₂ || s₁ == s₂ && decide (i₁ < i₂) || s₁ == s₂ && i₁ == i₂ && decide (a₁ < a₂))
• x✝¹.lt x✝ = decide (x✝¹.ctorIdx < x✝.ctorIdx)

instance Lean.Meta.DiscrTree.instLTKey : LT Key

Equations

• Lean.Meta.DiscrTree.instLTKey = { lt := fun (a b : Lean.Meta.DiscrTree.Key) => a.lt b = true }

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

Equations

• Lean.Meta.DiscrTree.instDecidableLtKey a b = inferInstanceAs (Decidable (a.lt b = true))

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

Equations

• Lean.Meta.DiscrTree.Key.star.format = Std.Format.text "*"
• Lean.Meta.DiscrTree.Key.other.format = Std.Format.text "◾"
• (Lean.Meta.DiscrTree.Key.lit (Lean.Literal.natVal v)).format = Std.format v
• (Lean.Meta.DiscrTree.Key.lit (Lean.Literal.strVal v)).format = repr v
• (Lean.Meta.DiscrTree.Key.const k a).format = Std.format k
• (Lean.Meta.DiscrTree.Key.proj s i a).format = Std.format s ++ Std.Format.text "." ++ Std.format i
• (Lean.Meta.DiscrTree.Key.fvar k a).format = Std.format k.name
• Lean.Meta.DiscrTree.Key.arrow.format = Std.Format.text "∀"

instance Lean.Meta.DiscrTree.instToFormatKey : ToFormat Key

Equations

• Lean.Meta.DiscrTree.instToFormatKey = { format := Lean.Meta.DiscrTree.Key.format }

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

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

Equations

• Lean.Meta.DiscrTree.instToFormatTrie = { format := Lean.Meta.DiscrTree.Trie.format }

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

Equations

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

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

Equations

• Lean.Meta.DiscrTree.instToFormat = { format := Lean.Meta.DiscrTree.format }

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.

Equations

• Lean.Meta.DiscrTree.keysAsPattern keys = (Lean.Meta.DiscrTree.keysAsPattern.go✝ false).run' keys.toList

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

Equations

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

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

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

Equations

• d.insertCore keys v = d.insertKeyValue keys v