content: {-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs, KindSignatures #-}
  
  module Vect where
  
  data Nat = Z | S Nat
  
  type family   (n :: Nat) :+ (m :: Nat) :: Nat
  type instance Z :+ m = m
  type instance S n :+ m = S (n :+ m)
  
  data Vect :: Nat -> * -> * where
    VNil :: Vect Z a
    (:::) :: a -> Vect n a -> Vect (S n) a
  
  vAppend :: Vect n a -> Vect m a -> Vect (n :+ m) a
  vAppend x y = _vAppend_body
  
  lAppend :: [a] -> [a] -> [a]
  lAppend x y = _lAppend_body
  
  data MyList a = Nil | Cons a (MyList a)
  
  mlAppend :: MyList a -> MyList a -> MyList a
  mlAppend x y = _mlAppend_body
  
  mlAppend2 :: MyList a -> MyList a -> MyList a
  mlAppend2 x y = case x of
                    x' -> _mlAppend_body
  
  mlReverse :: MyList a -> MyList a
  mlReverse xs = mlReverse' xs Nil
    where
      mlReverse' :: MyList a -> MyList a -> MyList a
      mlReverse' xs' accum = _mlReverse_body
  
  mlReverse2 :: MyList a -> MyList a
  mlReverse2 xs = let mlReverse' :: MyList a -> MyList a -> MyList a
                      mlReverse' xs' accum = _mlReverse_body
                   in mlReverse' xs Nil
  