blob: 0ea3633fa34f77ad3cbe8aafa0ee1bc8690e6ae7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
{-# LANGUAGE GADTs #-}
module ShouldSucceed4 where
data Z
data S a
data Add n m r where
PZero :: Add Z m m
PSucc :: Add n m p -> Add (S n) m (S p)
data XList n a where
XNil :: XList Z a
XCons :: a -> XList n a -> XList (S n) a
-- simple safe append function
append :: (Add n m r) -> XList n a -> XList m a -> XList r a
append PZero XNil l = l
append (PSucc prf) (XCons x xs) l = XCons x (append prf xs l)
|
