files/practicum/BewijsInitTake.icl

   1 Zij gegeven:
   2
   3         init :: [a] -> [a]
   4         init [x]                = []                                            (1)
   5         init [x:xs]             = [x:init xs]                           (2)
   6
   7         take :: Int [a] -> [a]
   8         take 0 xs               = []                                            (3)
   9         take n []               = []                                            (4)
  10         take n [x:xs]   = [x : take (n-1) xs]           (5)
  11
  12         length :: [a] -> Int
  13         length []               = 0                                                     (6)
  14         length [x:xs]   = 1 + length xs                         (7)
  15
  16         (f o g) x               = f (g x)                                       (8)
  17
  18 Bewijs de volgende stelling voor alle eindige, niet-lege lijsten xs:
  19
  20         init xs = take (length xs - 1) xs
  21
  22 Je mag aannemen dat het Int-bereik onbeperkt is.