diff options
| -rw-r--r-- | test-suite/output/Intuition.out | 3 | ||||
| -rw-r--r-- | test-suite/output/Naming.out | 34 | ||||
| -rw-r--r-- | test-suite/output/set.out | 7 |
3 files changed, 10 insertions, 34 deletions
diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out index 5831c9f43..e99d9fdeb 100644 --- a/test-suite/output/Intuition.out +++ b/test-suite/output/Intuition.out @@ -1,7 +1,6 @@ 1 subgoal - m : Z - n : Z + m, n : Z H : (m >= n)%Z ============================ (m >= m)%Z diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index 105940a45..f0d2562e0 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -6,11 +6,7 @@ (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 1 subgoal - x3 : nat - x : nat - x1 : nat - x4 : nat - x0 : nat + x3, x, x1, x4, x0 : nat H : forall x x3 : nat, x + x1 = x4 + x3 ============================ x + x1 = x4 + x0 @@ -33,11 +29,7 @@ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - x3 : nat - x : nat - x1 : nat - x4 : nat - x0 : nat + x3, x, x1, x4, x0 : nat ============================ (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> @@ -46,11 +38,7 @@ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - x3 : nat - x : nat - x1 : nat - x4 : nat - x0 : nat + x3, x, x1, x4, x0 : nat H : forall x x3 : nat, x + x1 = x4 + x3 -> forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) @@ -59,25 +47,17 @@ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - x3 : nat - x : nat - x1 : nat - x4 : nat - x0 : nat + x3, x, x1, x4, x0 : nat H : forall x x3 : nat, x + x1 = x4 + x3 -> - forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (Datatypes.S x + x1) H0 : x + x1 = x4 + x0 - x5 : nat - x6 : nat - x7 : nat - S : nat + x5, x6, x7, S : nat ============================ x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - x3 : nat - a : nat + x3, a : nat H : a = 0 -> forall a : nat, a = 0 ============================ a = 0 diff --git a/test-suite/output/set.out b/test-suite/output/set.out index 333fbb86d..4dfd2bc22 100644 --- a/test-suite/output/set.out +++ b/test-suite/output/set.out @@ -6,16 +6,13 @@ x = x 1 subgoal - y1 := 0 : nat - y2 := 0 : nat + y1, y2 := 0 : nat x := y2 + 0 : nat ============================ x = x 1 subgoal - y1 := 0 : nat - y2 := 0 : nat - y3 := 0 : nat + y1, y2, y3 := 0 : nat x := y2 + y3 : nat ============================ x = x |