-- I have replaced Set by Type in order to be more in accordance with what was learned in the 
-- lecture.

Char :: Type 
     = data a | b | c | d | e | f | g | h | i | j | k | l | m | n | o | p | q | r | s | t | u | v | w | x | y | z


a :: Char 
  = a@_

b :: Char 
  = b@_

c :: Char 
  = c@_

d :: Char 
  = d@_

e :: Char 
  = e@_

f :: Char 
  = f@_

g :: Char 
  = g@_

h :: Char 
  = h@_

i :: Char 
  = i@_

j :: Char 
  = j@_

k :: Char 
  = k@_

l :: Char 
  = l@_

m :: Char 
  = m@_

n :: Char 
  = n@_

o :: Char 
  = o@_

p :: Char 
  = p@_

q :: Char 
  = q@_

r :: Char 
  = r@_

s :: Char 
  = s@_

t :: Char 
  = t@_

u :: Char 
  = u@_

v :: Char 
  = v@_

w :: Char 
  = w@_

x :: Char 
  = x@_

y :: Char 
  = y@_

z :: Char 
  = z@_


String :: Type 
       =  data nil | cons (c:: Char) (s :: String) 

nil :: String
    =  nil@_

cons (c:: Char)
     (s:: String)
     :: String
     = cons@_ c s



(+)    (x :: String)
       (y :: String)
       :: String
       = case x of {
           (nil) -> y;
           (cons c x') -> cons c (x' + y);}



double  (x:: String)
        :: String
        = {! !}

Test :: Type 
  = {!double (cons h (cons e (cons l (cons l (cons o nil))))) !}