@@ -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
23+--------------------------------------------------------------------------------
25+--------------------------------------------------------------------------------
27+length : Vect n a -> Nat
29+length (x::xs) = 1 + length xs
23--------------------------------------------------------------------------------
31--------------------------------------------------------------------------------
24-- Indexing into vectors
32-- Indexing into vectors
25--------------------------------------------------------------------------------
33--------------------------------------------------------------------------------