Documentation

Lean.Meta.DiscrTreeTypes

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

Discrimination tree key. See DiscrTree

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

          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