Small documentation updates
commitb6c9ef8334fa123474897fd495b00c6cecfe0d33
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 3 Aug 2015, 01:25 (11 years ago)
parent5a08c2c
libs/base/Data/VectType.idr+6−1
@@ -9,8 +9,13 @@ namespace Vect {
99
1010infixr 7 ::
1111
12−%elim data Vect : Nat -> Type -> Type where
12+||| Vectors: Generic lists with explicit length in the type
13+%elim
14+data Vect : Nat -> Type -> Type where
15+ ||| Empty vector
1316 Nil : Vect Z a
17+ ||| A non-empty vector of length `S n`, consisting of a head element and
18+ ||| the rest of the list, of length `n`.
1419 (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
1520
1621-- Hints for interactive editing
libs/prelude/Prelude/List.idr+4−3
@@ -18,11 +18,12 @@ import Prelude.Nat
1818infix 5 \\
1919infixr 7 ::,++
2020
21−||| Linked lists
21+||| Generic lists
2222%elim data List elem =
23− ||| The empty list
23+ ||| Empty list
2424 Nil |
25− ||| Cons cell
25+ ||| A non-empty list, consisting of a head element and the rest of
26+ ||| the list.
2627 (::) elem (List elem)
2728
2829-- Name hints for interactive editing
libs/prelude/Prelude/Nat.idr+2−1
@@ -12,7 +12,8 @@ import Prelude.Uninhabited
1212%access public
1313%default total
1414
15−||| Unary natural numbers
15+||| Natural numbers: unbounded, unsigned integers which can be pattern
16+||| matched.
1617%elim data Nat =
1718 ||| Zero
1819 Z |