git.iko.soy/Idris-dev
on master help sign in
Add parity functions for naturals. (#4201)
5562c93Vanessa McHale
libs/contrib/Data/Nat/Parity.idrnew file+16
compare with master
unifiedsplit
@@ -0,0 +1,16 @@
1+module Data.Nat.Parity
2+
3+%access public export
4+
5+--------------------------------------------------------------------------------
6+-- Parity
7+--------------------------------------------------------------------------------
8+
9+mutual
10+ even : Nat -> Bool
11+ even Z = True
12+ even (S k) = odd k
13+
14+ odd : Nat -> Bool
15+ odd Z = False
16+ odd (S k) = even k
libs/contrib/contrib.ipkg+1
@@ -38,6 +38,7 @@ modules = CFFI
38 , Data.Matrix.Algebraic
38 , Data.Matrix.Algebraic
39 , Data.Matrix.Numeric
39 , Data.Matrix.Numeric
40
40
41+ , Data.Nat.Parity
41 , Data.Nat.DivMod
42 , Data.Nat.DivMod
42 , Data.Nat.DivMod.IteratedSubtraction
43 , Data.Nat.DivMod.IteratedSubtraction
43
44