diff --git a/CHANGELOG.md b/CHANGELOG.md index 8d18f3096..ae2a37999 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -175,6 +175,7 @@ * Adds `leftmost` and `rightmost` to `Control.Order`, a generalisation of `min` and `max`. +* Adds `even` and `odd` to `Data.Integral`. * `Eq` and `Ord` implementations for `Fin n` now run in constant time. * Adds `getTermCols` and `getTermLines` to the base library. They return the diff --git a/libs/base/Data/Integral.idr b/libs/base/Data/Integral.idr new file mode 100644 index 000000000..876ac63a0 --- /dev/null +++ b/libs/base/Data/Integral.idr @@ -0,0 +1,9 @@ +module Data.Integral + +export +even : Integral n => Eq n => n -> Bool +even n = n `mod` 2 == 0 + +export +odd : Integral n => Eq n => n -> Bool +odd = not . even diff --git a/tests/base/data_integral/Integral.idr b/tests/base/data_integral/Integral.idr new file mode 100644 index 000000000..f7c16efdf --- /dev/null +++ b/tests/base/data_integral/Integral.idr @@ -0,0 +1,52 @@ +import Data.Integral + +Cases : Type +Cases = List Bool + +natEvenCases : Cases +natEvenCases = [ + even 0, + even 2, + even 4, + even Z, + even (S (S Z)) + ] + +natOddCases : Cases +natOddCases = [ + odd 1, + odd 3, + odd 5, + odd (S Z), + odd (S (S (S Z))) + ] + +integralEvenCases : Cases +integralEvenCases = [ + even (-4), + even (-2), + even 0, + even 2, + even 4 +] + +integralOddCases : Cases +integralOddCases = [ + odd (-5), + odd (-3), + odd (-1), + odd 1, + odd 3, + odd 5 +] + +main : IO () +main = do + printLn "Nat Even" + printLn natEvenCases + printLn "Nat Odd" + printLn natOddCases + printLn "Integral Even" + printLn integralEvenCases + printLn "Integral Odd" + printLn integralOddCases diff --git a/tests/base/data_integral/expected b/tests/base/data_integral/expected new file mode 100644 index 000000000..39ffccc9e --- /dev/null +++ b/tests/base/data_integral/expected @@ -0,0 +1,10 @@ +1/1: Building Integral (Integral.idr) +Main> "Nat Even" +[True, True, True, True, True] +"Nat Odd" +[True, True, True, True, True] +"Integral Even" +[True, True, True, True, True] +"Integral Odd" +[True, True, True, True, True, True] +Main> Bye for now! diff --git a/tests/base/data_integral/input b/tests/base/data_integral/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/base/data_integral/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/base/data_integral/run b/tests/base/data_integral/run new file mode 100644 index 000000000..1271d4512 --- /dev/null +++ b/tests/base/data_integral/run @@ -0,0 +1,3 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner Integral.idr < input