Fix case-split spec for 706

This commit is contained in:
Nikolay Yakimov
2016-07-10 17:43:08 +03:00
parent 0e788e295c
commit 1a302707b3
2 changed files with 69 additions and 0 deletions

View File

@@ -0,0 +1,39 @@
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs, KindSignatures #-}
module Vect706 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 = undefined
lAppend :: [a] -> [a] -> [a]
lAppend x y = undefined
data MyList a = Nil | Cons a (MyList a)
mlAppend :: MyList a -> MyList a -> MyList a
mlAppend x y = undefined
mlAppend2 :: MyList a -> MyList a -> MyList a
mlAppend2 x y = case x of
x' -> undefined
mlReverse :: MyList a -> MyList a
mlReverse xs = mlReverse' xs Nil
where
mlReverse' :: MyList a -> MyList a -> MyList a
mlReverse' xs' accum = undefined
mlReverse2 :: MyList a -> MyList a
mlReverse2 xs = let mlReverse' :: MyList a -> MyList a -> MyList a
mlReverse' xs' accum = undefined
in mlReverse' xs Nil