Commit cf09f92c authored by Michael Hanus 's avatar Michael Hanus
Browse files

Introduces recursive definition of length since it is better usable for verification

parent 14acea7e
......@@ -331,15 +331,18 @@ null (_:_) = False
(x:xs) ++ ys = x : xs++ys
--- Computes the length of a list.
--length :: [_] -> Int
--length [] = 0
--length (_:xs) = 1 + length xs
length :: [_] -> Int
length [] = 0
length (_:xs) = 1 + length xs
{-
-- This version is more efficient but less usable for verification:
length :: [_] -> Int
length xs = len xs 0
where
len [] n = n
len (_:ys) n = let np1 = n + 1 in len ys $!! np1
-}
--- List index (subscript) operator, head has index 0.
(!!) :: [a] -> Int -> a
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment