/Prelude-v17.0.0/List/length

Copy path to clipboard

Examples

length Natural [ 0, 1, 2 ] ≡ 3
length Natural ([] : List Natural) ≡ 0

Source

{-
Returns the number of elements in a list
-}
let length
: ∀(a : Type) → List a → Natural
= List/length

let example0 = assert : length Natural [ 0, 1, 2 ] ≡ 3

let example1 = assert : length Natural ([] : List Natural) ≡ 0

in length