twee 2.1.3 → 2.1.4
raw patch · 3 files changed
+16/−2 lines, 3 filesdep ~twee-lib
Dependency ranges changed: twee-lib
Files
- executable/Main.hs +4/−0
- tests/ROB033-1.p +10/−0
- twee.cabal +2/−2
executable/Main.hs view
@@ -605,7 +605,11 @@ hSetBuffering stdout LineBuffering join . parseCommandLineWithExtraArgs ["--no-conjunctive-conjectures", "--no-split"]+#ifdef VERSION_twee "Twee, an equational theorem prover" . version ("twee version " ++ VERSION_twee) $+#else+ "Twee, an equational theorem prover" . version "twee development version" $+#endif globalFlags *> parseMainFlags *> -- hack: get --quiet and --no-proof options to appear before --tstp forAllFilesBox <*>
+ tests/ROB033-1.p view
@@ -0,0 +1,10 @@+cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).+cnf(associativity_of_add, axiom,+ add(add(X, Y), Z)=add(X, add(Y, Z))).+cnf(robbins_axiom, axiom,+ negate(add(negate(add(X, Y)), negate(add(X, negate(Y)))))=X).+cnf(sos04, axiom, g(A)=negate(add(A, negate(A)))).+cnf(sos05, axiom, h(A)=add(A, add(A, add(A, g(A))))).+cnf(goals, negated_conjecture,+ add(negate(add(x0, negate(x1))),+ negate(add(negate(x0), negate(x1))))!=x1).
twee.cabal view
@@ -1,5 +1,5 @@ name: twee-version: 2.1.3+version: 2.1.4 synopsis: An equational theorem prover homepage: http://github.com/nick8325/twee license: BSD3@@ -44,7 +44,7 @@ main-is: executable/Main.hs default-language: Haskell2010 build-depends: base < 5,- twee-lib == 2.1.3,+ twee-lib == 2.1.4, containers, pretty, split,