git.iko.soy/Idris-dev
on master help sign in
Add length to Vect
db22d5dJean-Remi Desjardins
libs/prelude/Prelude/Vect.idr+8
compare with master
unifiedsplit
@@ -20,6 +20,14 @@ infixr 7 ::
20-- Hints for interactive editing
20-- Hints for interactive editing
21%name Vect xs,ys,zs,ws
21%name Vect xs,ys,zs,ws
22
22
23+--------------------------------------------------------------------------------
24+-- Length
25+--------------------------------------------------------------------------------
26+
27+length : Vect n a -> Nat
28+length [] = 0
29+length (x::xs) = 1 + length xs
30+
23--------------------------------------------------------------------------------
31--------------------------------------------------------------------------------
24-- Indexing into vectors
32-- Indexing into vectors
25--------------------------------------------------------------------------------
33--------------------------------------------------------------------------------