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

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

Discrimination tree key. See DiscrTree

Instances For
    instance Lean.Meta.DiscrTree.instBEqKey :
    {simpleReduce : Bool} → BEq (Lean.Meta.DiscrTree.Key simpleReduce)
    instance Lean.Meta.DiscrTree.instReprKey :
    {simpleReduce : Bool} → Repr (Lean.Meta.DiscrTree.Key simpleReduce)
    inductive Lean.Meta.DiscrTree.Trie (α : Type) (simpleReduce : Bool) :

    Discrimination tree trie. See DiscrTree.

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

      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.


      • 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 ( 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
      Instances For