Add parity functions for naturals. (#4201)
* Add even/odd function for naturals
commit5562c93d58de7f9c19b94b2896b75ee71f731ee1
authorVanessa McHale <vmchale@users.noreply.github.com>
dateMon 20 Nov 2017, 02:21 (9 years ago)
parent8f8c93f
libs/contrib/Data/Nat/Parity.idrnew file+16
@@ -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
3838 , Data.Matrix.Algebraic
3939 , Data.Matrix.Numeric
4040
41+ , Data.Nat.Parity
4142 , Data.Nat.DivMod
4243 , Data.Nat.DivMod.IteratedSubtraction
4344