@@ -20,6 +20,14 @@ infixr 7 ::
2020-- Hints for interactive editing
2121%name Vect xs,ys,zs,ws
2222
23+--------------------------------------------------------------------------------
24+-- Length
25+--------------------------------------------------------------------------------
26+
27+length : Vect n a -> Nat
28+length [] = 0
29+length (x::xs) = 1 + length xs
30+
2331--------------------------------------------------------------------------------
2432-- Indexing into vectors
2533--------------------------------------------------------------------------------