See file DiscrTree.lean
for the actual implementation and documentation.
Notes regarding term reduction at the DiscrTree
module.
- In
simp
, we want to havesimp
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
Discrimination trees. It is an index from terms to values of type α
.
- root : PersistentHashMap Key (Trie α)