Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- data Vect :: Nat -> * -> * where
- Cons :: KnownNat n => a -> Vect (n - 1) a -> Vect n a
- Nil :: (KnownNat n, 0 <= n) => Vect n a
- k :: Vect 1 Int
- k = Cons 1 Nil
- u :: Vect 0 Int
- u = Nil
- j = vhead k
- p = vtail k
- vhead :: KnownNat n => Vect (n + 1) a -> a
- vhead (Cons x _) = x
- vtail :: (KnownNat n, n ~ (n + 1 - 1)) => Vect (n + 1) a -> Vect n a
- vtail Nil = Nil
- vtail (Cons _ xs) = xs
- vzip :: Vect n a -> Vect n b -> Vect n (a, b)
- vzip Nil Nil = Nil
- vzip (Cons x xs) (Cons y ys) = Cons (x, y) $ vzip xs ys
- vindex :: (KnownNat n, KnownNat i, i <= n - 1) => Proxy i -> Vect n a -> a
- vindex (pi :: Proxy i) (Cons x xs) =
- case natVal pi of
- 0 -> x
- _ -> vindex (Proxy :: Proxy (i - 1)) xs
Add Comment
Please, Sign In to add comment