diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Search.out | 36 | ||||
| -rw-r--r-- | test-suite/output/Search.v | 6 | ||||
| -rw-r--r-- | test-suite/output/SearchPattern.out | 20 |
3 files changed, 31 insertions, 31 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 2a22a89b66..120c6a4ea6 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -1,29 +1,29 @@ -le_S: forall n m : nat, n <= m -> n <= S m le_n: forall n : nat, n <= n +le_S: forall n m : nat, n <= m -> n <= S m le_pred: forall n m : nat, n <= m -> pred n <= pred m le_S_n: forall n m : nat, S n <= S m -> n <= m -false: bool true: bool -xorb: bool -> bool -> bool +false: bool +andb: bool -> bool -> bool orb: bool -> bool -> bool -negb: bool -> bool implb: bool -> bool -> bool -andb: bool -> bool -> bool -pred_Sn: forall n : nat, n = pred (S n) -plus_n_Sm: forall n m : nat, S (n + m) = n + S m -plus_n_O: forall n : nat, n = n + 0 -plus_Sn_m: forall n m : nat, S n + m = S (n + m) -plus_O_n: forall n : nat, 0 + n = n -mult_n_Sm: forall n m : nat, n * m + n = n * S m -mult_n_O: forall n : nat, 0 = n * 0 -min_r: forall n m : nat, m <= n -> min n m = m -min_l: forall n m : nat, n <= m -> min n m = n -max_r: forall n m : nat, n <= m -> max n m = m -max_l: forall n m : nat, m <= n -> max n m = n +xorb: bool -> bool -> bool +negb: bool -> bool +eq_S: forall x y : nat, x = y -> S x = S y f_equal_pred: forall x y : nat, x = y -> pred x = pred y +pred_Sn: forall n : nat, n = pred (S n) +eq_add_S: forall n m : nat, S n = S m -> n = m f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 +plus_n_O: forall n : nat, n = n + 0 +plus_O_n: forall n : nat, 0 + n = n +plus_n_Sm: forall n m : nat, S (n + m) = n + S m +plus_Sn_m: forall n m : nat, S n + m = S (n + m) f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 -eq_add_S: forall n m : nat, S n = S m -> n = m -eq_S: forall x y : nat, x = y -> S x = S y +mult_n_O: forall n : nat, 0 = n * 0 +mult_n_Sm: forall n m : nat, n * m + n = n * S m +max_l: forall n m : nat, m <= n -> max n m = n +max_r: forall n m : nat, n <= m -> max n m = m +min_l: forall n m : nat, n <= m -> min n m = n +min_r: forall n m : nat, m <= n -> min n m = m diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index f1489f22ae..4ef2634733 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -1,5 +1,5 @@ (* Some tests of the Search command *) -Search le. (* app nodes *) -Search bool. (* no apps *) -Search (@eq nat). (* complex pattern *) +SearchHead le. (* app nodes *) +SearchHead bool. (* no apps *) +SearchHead (@eq nat). (* complex pattern *) diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index d546f84daa..6595302e13 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -1,32 +1,32 @@ -false: bool true: bool -xorb: bool -> bool -> bool +false: bool +andb: bool -> bool -> bool orb: bool -> bool -> bool -negb: bool -> bool implb: bool -> bool -> bool -andb: bool -> bool -> bool -S: nat -> nat +xorb: bool -> bool -> bool +negb: bool -> bool O: nat +S: nat -> nat +length: forall A : Type, list A -> nat pred: nat -> nat plus: nat -> nat -> nat mult: nat -> nat -> nat minus: nat -> nat -> nat -min: nat -> nat -> nat max: nat -> nat -> nat -length: forall A : Type, list A -> nat +min: nat -> nat -> nat S: nat -> nat pred: nat -> nat plus: nat -> nat -> nat mult: nat -> nat -> nat minus: nat -> nat -> nat -min: nat -> nat -> nat max: nat -> nat -> nat +min: nat -> nat -> nat mult_n_Sm: forall n m : nat, n * m + n = n * S m -le_n: forall n : nat, n <= n identity_refl: forall (A : Type) (a : A), identity a a -eq_refl: forall (A : Type) (x : A), x = x iff_refl: forall A : Prop, A <-> A +eq_refl: forall (A : Type) (x : A), x = x +le_n: forall n : nat, n <= n pair: forall A B : Type, A -> B -> A * B conj: forall A B : Prop, A -> B -> A /\ B |