implement `Prelude.List.length` using `Nat` constructors
Unless there was a reason for implementing it with `0` and `(1 +)`,
it seems more "natural" to use `Z` and `S` since this function returns
a `Nat`.
This improves the output of the REPL command `:printdef Prelude.List.length`,
which previously showed as the following:
```
Idris> :printdef Prelude.List.length
length : List a -> Nat
length [] = PE_fromInteger_dc75de74 0
length (x :: xs) = PE_+_6b31ad5c (PE_fromInteger_dc75de74 1) (length xs)
```
Signed-off-by: Michael Morgan <morgan.michael@me.com>
commit242191e325e943256340558753809f63b0a1dd62
authorMichael Morgan <morgan.michael@me.com>
dateFri 17 Nov 2017, 11:47 (9 years ago)
parent21ab196
libs/prelude/Prelude/List.idr+2−2
@@ -95,8 +95,8 @@ inBounds (S k) (x :: xs) with (inBounds k xs)
9595|||
9696||| Runs in linear time
9797length : List a -> Nat
98−length [] = 0
99−length (x::xs) = 1 + length xs
98+length [] = Z
99+length (x::xs) = S (length xs)
100100
101101--------------------------------------------------------------------------------
102102-- Indexing into lists