Small documentation updates

libs/base/Data/VectType.idr

@@ -9,8 +9,13 @@ namespace Vect {
 
 infixr 7 ::
 
-%elim data Vect : Nat -> Type -> Type where
+||| Vectors: Generic lists with explicit length in the type
+%elim 
+data Vect : Nat -> Type -> Type where
+  ||| Empty vector 
   Nil  : Vect Z a
+  ||| A non-empty vector of length `S n`, consisting of a head element and 
+  ||| the rest of the list, of length `n`.
   (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
 
 -- Hints for interactive editing

libs/prelude/Prelude/List.idr

@@ -18,11 +18,12 @@ import Prelude.Nat
 infix 5 \\
 infixr 7 ::,++
 
-||| Linked lists
+||| Generic lists
 %elim data List elem =
-  ||| The empty list
+  ||| Empty list
   Nil |
-  ||| Cons cell
+  ||| A non-empty list, consisting of a head element and the rest of
+  ||| the list.
   (::) elem (List elem)
 
 -- Name hints for interactive editing

libs/prelude/Prelude/Nat.idr

@@ -12,7 +12,8 @@ import Prelude.Uninhabited
 %access public
 %default total
 
-||| Unary natural numbers
+||| Natural numbers: unbounded, unsigned integers which can be pattern
+||| matched.
 %elim data Nat =
   ||| Zero
   Z |