Add a couple of doc comments
commitf3f828c82b545bfd03854668871373fc5f4d609c
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 15 Aug 2015, 23:10 (11 years ago)
parent15d3674
libs/base/Data/Fin.idr+2
@@ -129,6 +129,8 @@ natToFin (S k) (S j) with (natToFin k j)
129129 | Nothing = Nothing
130130natToFin _ _ = Nothing
131131
132+||| Convert an `Integer` to a `Fin`, provided the integer is within bounds.
133+||| @n The upper bound of the Fin
132134integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
133135integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!
134136integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
libs/prelude/Prelude/Maybe.idr+6−2
@@ -11,9 +11,13 @@ import Prelude.Foldable
1111%access public
1212%default total
1313
14+||| An optional value. This can be used to represent the possibility of
15+||| failure, where a function may return a value, or not.
1416data Maybe a
15− = Nothing
16− | Just a
17+ = ||| No value stored
18+ Nothing
19+ | ||| A value of type `a` is stored
20+ Just a
1721
1822--------------------------------------------------------------------------------
1923-- Syntactic tests