Commit a856647a authored by simonmar's avatar simonmar

[project @ 2005-04-28 10:13:44 by simonmar]

mode=slow
parent 0e1b113e
......@@ -33,6 +33,8 @@ application of that function may be rewritten.
module Main (main) where
import System.Environment
data Term = Var Id |
Fun Id [Term] [Lemma]
......@@ -227,10 +229,12 @@ actually relevant to the truth of the theorem. In fact none of them
can be rewritten in any interesting way.
\begin{code}
main = print test
main = do
(n:_) <- getArgs
print (test (read n))
test :: Bool
test = all test0 (take 20 (repeat (Var X)))
test :: Int -> Bool
test n = all test0 (take n (repeat (Var X)))
test0 xxxx = tautp (apply_subst subst0 theorem)
where
......
......@@ -3,3 +3,6 @@ include $(TOP)/mk/boilerplate.mk
-include opts.mk
include $(TOP)/mk/target.mk
FAST_OPTS = 20
NORM_OPTS = 20
SLOW_OPTS = 300
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment