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

inductive Lean.Meta.DiscrTree.Key (simpleReduce : Bool) : Type

• const: {simpleReduce : Bool} → Lake.Name → Nat → Lean.Meta.DiscrTree.Key simpleReduce
• fvar: {simpleReduce : Bool} → Lean.FVarId → Nat → Lean.Meta.DiscrTree.Key simpleReduce
• lit: {simpleReduce : Bool} → Lean.Literal → Lean.Meta.DiscrTree.Key simpleReduce
• star: {simpleReduce : Bool} → Lean.Meta.DiscrTree.Key simpleReduce
• other: {simpleReduce : Bool} → Lean.Meta.DiscrTree.Key simpleReduce
• arrow: {simpleReduce : Bool} → Lean.Meta.DiscrTree.Key simpleReduce
• proj: {simpleReduce : Bool} → Lake.Name → Nat → Nat → Lean.Meta.DiscrTree.Key simpleReduce

Discrimination tree key. See DiscrTree

instance Lean.Meta.DiscrTree.instInhabitedKey : {a : Bool} → Inhabited (Lean.Meta.DiscrTree.Key a)

Equations

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

instance Lean.Meta.DiscrTree.instBEqKey : {simpleReduce : Bool} → BEq (Lean.Meta.DiscrTree.Key simpleReduce)

Equations

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

instance Lean.Meta.DiscrTree.instReprKey : {simpleReduce : Bool} → Repr (Lean.Meta.DiscrTree.Key simpleReduce)

Equations

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

def Lean.Meta.DiscrTree.Key.hash {s : Bool} : Lean.Meta.DiscrTree.Key s → UInt64

Equations

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

instance Lean.Meta.DiscrTree.instHashableKey {s : Bool} : Hashable (Lean.Meta.DiscrTree.Key s)

Equations

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

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

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

Discrimination tree trie. See DiscrTree.

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

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

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

If simpleReduce := true, then only simple reduction are performed while indexing/retrieving terms. For example, iota reduction is not performed.

We use simpleReduce := false in the type class resolution module, and simpleReduce := true in simp.

Motivations:

• 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.

• During type class resolution, we often want to reduce types using even iota. 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