小编Duf*_*aer的帖子

使用 GADT，我定义了一个深度索引树数据类型（2-3 tree）。深度是静态地确保树木平衡的。

-- Natural numbers
data Nat = Z | S Nat

-- Depth-indexed 2-3 tree
data DT :: Nat -> Type -> Type where
  -- Pattern of node names: N{#subtrees}_{#containedValues}
  N0_0 :: DT Z a
  N2_1 :: DT n a -> a -> DT n a
    -> DT (S n) a
  N3_2 :: DT n a -> a -> DT n a -> a -> DT n a
    -> DT (S n) a

deriving instance Eq …