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

inductive Lean.Meta.DiscrTree.Key : Type

Discrimination tree key. See DiscrTree

• star : Key
• other : Key
• lit : Literal → Key
• fvar : FVarId → Nat → Key
• const : Name → Nat → Key
• arrow : Key
• proj : Name → Nat → Nat → Key

instance Lean.Meta.DiscrTree.instInhabitedKey : Inhabited Key

Equations

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

def Lean.Meta.DiscrTree.instInhabitedKey.default : Key

Equations

• Lean.Meta.DiscrTree.instInhabitedKey.default = Lean.Meta.DiscrTree.Key.star

def Lean.Meta.DiscrTree.instBEqKey.beq : Key → Key → Bool

Equations

• Lean.Meta.DiscrTree.instBEqKey.beq Lean.Meta.DiscrTree.Key.star Lean.Meta.DiscrTree.Key.star = true
• Lean.Meta.DiscrTree.instBEqKey.beq Lean.Meta.DiscrTree.Key.other Lean.Meta.DiscrTree.Key.other = true
• Lean.Meta.DiscrTree.instBEqKey.beq (Lean.Meta.DiscrTree.Key.lit a) (Lean.Meta.DiscrTree.Key.lit b) = (a == b)
• Lean.Meta.DiscrTree.instBEqKey.beq (Lean.Meta.DiscrTree.Key.fvar a a_1) (Lean.Meta.DiscrTree.Key.fvar b b_1) = (a == b && a_1 == b_1)
• Lean.Meta.DiscrTree.instBEqKey.beq (Lean.Meta.DiscrTree.Key.const a a_1) (Lean.Meta.DiscrTree.Key.const b b_1) = (a == b && a_1 == b_1)
• Lean.Meta.DiscrTree.instBEqKey.beq Lean.Meta.DiscrTree.Key.arrow Lean.Meta.DiscrTree.Key.arrow = true
• Lean.Meta.DiscrTree.instBEqKey.beq (Lean.Meta.DiscrTree.Key.proj a a_1 a_2) (Lean.Meta.DiscrTree.Key.proj b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Meta.DiscrTree.instBEqKey.beq x✝¹ x✝ = false

instance Lean.Meta.DiscrTree.instBEqKey : BEq Key

Equations

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

instance Lean.Meta.DiscrTree.instReprKey : Repr Key

Equations

• Lean.Meta.DiscrTree.instReprKey = { reprPrec := Lean.Meta.DiscrTree.instReprKey.repr }

def Lean.Meta.DiscrTree.instReprKey.repr : Key → Nat → Format

Equations

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

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

Equations

• (Lean.Meta.DiscrTree.Key.const n a).hash = mixHash 5237 (mixHash (hash n) (hash a))
• (Lean.Meta.DiscrTree.Key.fvar n a).hash = mixHash 3541 (mixHash (hash n) (hash a))
• (Lean.Meta.DiscrTree.Key.lit v).hash = mixHash 1879 (hash v)
• Lean.Meta.DiscrTree.Key.star.hash = 7883
• Lean.Meta.DiscrTree.Key.other.hash = 2411
• Lean.Meta.DiscrTree.Key.arrow.hash = 17
• (Lean.Meta.DiscrTree.Key.proj s i a).hash = mixHash (hash a) (mixHash (hash s) (hash i))

instance Lean.Meta.DiscrTree.instHashableKey : Hashable Key

Equations

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

instance Lean.Meta.DiscrTree.instToExprKey : ToExpr Key

Equations

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

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

Discrimination tree trie. See DiscrTree.

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

Notes regarding term reduction at the DiscrTree module.

• In simp, we want to have simp theorem such as

@[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
    Quot.liftOn (Quot.mk r a) f h = f a := rfl

If we enable iota, then the lhs is reduced to f a. Note that when retrieving terms, we may also disable beta and zeta reduction. See issue https://github.com/leanprover/lean4/issues/2669

• During type class resolution, we often want to reduce types using even iota and projection reduction. Example:

inductive Ty where
  | int
  | bool

@[reducible] def Ty.interp (ty : Ty) : Type :=
  Ty.casesOn (motive := fun _ => Type) ty Int Bool

def test {a b c : Ty} (f : a.interp → b.interp → c.interp) (x : a.interp) (y : b.interp) : c.interp :=
  f x y

def f (a b : Ty.bool.interp) : Ty.bool.interp :=
  -- We want to synthesize `BEq Ty.bool.interp` here, and it will fail
  -- if we do not reduce `Ty.bool.interp` to `Bool`.
  test (.==.) a b

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

Discrimination trees. It is an index from terms to values of type α.

• root : PersistentHashMap Key (Trie α)