@@ -95,8 +95,8 @@ inBounds (S k) (x :: xs) with (inBounds k xs)
96||| Runs in linear time
96||| Runs in linear time
97length : List a -> Nat
97length : List a -> Nat
98−length [] = 0
98+length [] = Z
99−length (x::xs) = 1 + length xs
99+length (x::xs) = S (length xs)
101--------------------------------------------------------------------------------
101--------------------------------------------------------------------------------
102-- Indexing into lists
102-- Indexing into lists