append :: (Vec n a) (Vec m a) -> Vec x a | Add n m x
append (Vec a) (Vec b) = Vec (a +++ b)
+<<<<<<< HEAD
//Start = nrepeat (Three :*: Three) 'a'
v1 :: Vec (Succ (Succ Zero)) Int
v2 :: Vec Three Int
v2 = repeat 5
+=======
+>>>>>>> 7675818dc8fc41eaf864dc89a8c2ce62c7dae93f
class Le a b ~c
where
le :: a b -> c
:: A = A; :: B = B; :: C = C; :: D = D; :: E = E; :: F = F; :: G = G; :: H = H;
:: I = I; :: J = J; :: K = K; :: L = L; :: M = M; :: N = N; :: O = O; :: P = P;
:: Q = Q; :: R = R; :: S = S; :: T = T; :: U = U; :: V = V; :: W = W; :: X = X;
+<<<<<<< HEAD
:: Y = Y; :: Z = Z; :: Spc = Spc
:: Nl = Nl
:: SC l r = SC
:: NilS :== ()
NilS :: NilS
NilS = undef
+=======
+:: Y = Y; :: Z = Z;
+:: Nul = Nul
+:: SC l r = SC
+
+Start = nrepeat (Three :*: Three) 'a'
+
+e1 :: Vec (Succ (Succ Zero)) Int
+e1 = append (single 1) (single 32)
+
+e2 :: Vec Three Int
+e2 = repeat 5
+>>>>>>> 7675818dc8fc41eaf864dc89a8c2ce62c7dae93f