-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathoddeven.hs
33 lines (32 loc) · 1.01 KB
/
oddeven.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
import Test.Speculate
main :: IO ()
main = speculate args
{ showConditions = True
, constants =
[ showConstant (0::Int)
, showConstant (1::Int)
, showConstant (2::Int)
, showConstant False
, showConstant True
, constant "odd" $ odd -:> int
, constant "even" $ even -:> int
, constant "`mod`" $ mod -:> int
, constant "==" $ (==) -:> int
]
{- after adding the following, conditions do not appear but in a way should:
, conditionAtoms =
[ constant "`mod`" $ mod -:> int
, constant "==" $ (==) -:> int
]
, equationAtoms =
[ constant "odd" $ odd -:> int
, constant "even" $ even -:> int
]
-- the problem is that "odd" and "even" are actually smaller versions of the
-- preconditions we "want":
-- > (x `mod` 2 == 0) == even x
-- conditionAtoms and equationAtoms should be used with care!
-- TODO: add that somewhere in the docs
-- TODO: make this not happen? would be really hard: theorize twice!
-}
}