Merge pull request #4202 from msmorgan/list-length-nat-constructors
implement `Prelude.List.length` using `Nat` constructors
commit5afea19150eb841d34445ccaa6757f45740c7d7d
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateMon 20 Nov 2017, 09:22 (9 years ago)
parent5562c93242191e
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