git.iko.soy/Idris-dev
on master help sign in
Add a couple of doc comments
f3f828cEdwin Brady
libs/base/Data/Fin.idr+2
compare with master
unifiedsplit
@@ -129,6 +129,8 @@ natToFin (S k) (S j) with (natToFin k j)
129 | Nothing = Nothing
129 | Nothing = Nothing
130natToFin _ _ = Nothing
130natToFin _ _ = Nothing
131
131
132+||| Convert an `Integer` to a `Fin`, provided the integer is within bounds.
133+||| @n The upper bound of the Fin
132integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
134integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
133integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!
135integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!
134integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
136integerToFin 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
11%access public
11%access public
12%default total
12%default total
13
13
14+||| An optional value. This can be used to represent the possibility of
15+||| failure, where a function may return a value, or not.
14data Maybe a
16data Maybe a
17+ = ||| No value stored
15− = Nothing
18+ Nothing
19+ | ||| A value of type `a` is stored
16− | Just a
20+ Just a
17
21
18--------------------------------------------------------------------------------
22--------------------------------------------------------------------------------
19-- Syntactic tests
23-- Syntactic tests