git.iko.soy/Idris-dev
on master help sign in
Nat: add examples to function documentation
da0a382Langston Barrett
libs/prelude/Prelude/Nat.idr+15
compare with master
unifiedsplit
@@ -310,9 +310,19 @@ fact (S n) = (S n) * fact n
310-- Division and modulus
310-- Division and modulus
311--------------------------------------------------------------------------------
311--------------------------------------------------------------------------------
312
312
313+||| The proof that no successor of a natural number can be zero.
314+|||
315+||| ```idris example
316+||| modNatNZ 10 3 SIsNotZ
317+||| ```
313SIsNotZ : {x: Nat} -> (S x = Z) -> Void
318SIsNotZ : {x: Nat} -> (S x = Z) -> Void
314SIsNotZ Refl impossible
319SIsNotZ Refl impossible
315
320
321+||| Modulus function where the divisor is not zero.
322+|||
323+||| ```idris example
324+||| modNatNZ 100 2 SIsNotZ
325+||| ```
316modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
326modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
317modNatNZ left Z p = void (p Refl)
327modNatNZ left Z p = void (p Refl)
318modNatNZ left (S right) _ = mod' left left right
328modNatNZ left (S right) _ = mod' left left right
@@ -329,6 +339,11 @@ partial
329modNat : Nat -> Nat -> Nat
339modNat : Nat -> Nat -> Nat
330modNat left (S right) = modNatNZ left (S right) SIsNotZ
340modNat left (S right) = modNatNZ left (S right) SIsNotZ
331
341
342+||| Division where the divisor is not zero.
343+|||
344+||| ```idris example
345+||| divNatNZ 100 2 SIsNotZ
346+||| ```
332divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
347divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
333divNatNZ left Z p = void (p Refl)
348divNatNZ left Z p = void (p Refl)
334divNatNZ left (S right) _ = div' left left right
349divNatNZ left (S right) _ = div' left left right