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

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

    Discrimination tree trie. See DiscrTree.

    Instances For

      Notes regarding term reduction at the DiscrTree module.

      @[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. Note that when retrieving terms, we may also disable beta and zeta reduction. See issue

      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) :

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

      Instances For