git.iko.soy/Idris-dev
on master help sign in
Small documentation updates
b6c9ef8Edwin Brady
libs/base/Data/VectType.idr+6−1
compare with master
unifiedsplit
@@ -9,8 +9,13 @@ namespace Vect {
9
9
10infixr 7 ::
10infixr 7 ::
11
11
12+||| Vectors: Generic lists with explicit length in the type
13+%elim
12−%elim data Vect : Nat -> Type -> Type where
14+data Vect : Nat -> Type -> Type where
15+ ||| Empty vector
13 Nil : Vect Z a
16 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`.
14 (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
19 (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
15
20
16-- Hints for interactive editing
21-- Hints for interactive editing
libs/prelude/Prelude/List.idr+4−3
@@ -18,11 +18,12 @@ import Prelude.Nat
18infix 5 \\
18infix 5 \\
19infixr 7 ::,++
19infixr 7 ::,++
20
20
21−||| Linked lists
21+||| Generic lists
22%elim data List elem =
22%elim data List elem =
23− ||| The empty list
23+ ||| Empty list
24 Nil |
24 Nil |
25− ||| Cons cell
25+ ||| A non-empty list, consisting of a head element and the rest of
26+ ||| the list.
26 (::) elem (List elem)
27 (::) elem (List elem)
27
28
28-- Name hints for interactive editing
29-- Name hints for interactive editing
libs/prelude/Prelude/Nat.idr+2−1
@@ -12,7 +12,8 @@ import Prelude.Uninhabited
12%access public
12%access public
13%default total
13%default total
14
14
15−||| Unary natural numbers
15+||| Natural numbers: unbounded, unsigned integers which can be pattern
16+||| matched.
16%elim data Nat =
17%elim data Nat =
17 ||| Zero
18 ||| Zero
18 Z |
19 Z |