diff options
| -rw-r--r-- | test-suite/output/Search.out | 42 | ||||
| -rw-r--r-- | test-suite/output/Search.v | 5 | ||||
| -rw-r--r-- | test-suite/output/SearchPattern.out | 48 | ||||
| -rw-r--r-- | test-suite/output/SearchPattern.v | 19 | ||||
| -rw-r--r-- | test-suite/output/SearchRewrite.out | 2 | ||||
| -rw-r--r-- | test-suite/output/SearchRewrite.v | 4 |
6 files changed, 120 insertions, 0 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out new file mode 100644 index 0000000000..93eff64c90 --- /dev/null +++ b/test-suite/output/Search.out @@ -0,0 +1,42 @@ +le_S: forall n m : nat, n <= m -> n <= S m +le_n: forall n : nat, n <= n +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 +sumor_beq: + forall (A : Type) (B : Prop), + (A -> A -> bool) -> (B -> B -> bool) -> A + {B} -> A + {B} -> bool +sumbool_beq: + forall A B : Prop, + (A -> A -> bool) -> (B -> B -> bool) -> {A} + {B} -> {A} + {B} -> bool +xorb: bool -> bool -> bool +sum_beq: + forall A B : Type, + (A -> A -> bool) -> (B -> B -> bool) -> A + B -> A + B -> bool +prod_beq: + forall A B : Type, + (A -> A -> bool) -> (B -> B -> bool) -> A * B -> A * B -> bool +orb: bool -> bool -> bool +option_beq: forall A : Type, (A -> A -> bool) -> option A -> option A -> bool +negb: bool -> bool +nat_beq: nat -> nat -> bool +list_beq: forall A : Type, (A -> A -> bool) -> list A -> list A -> bool +implb: bool -> bool -> bool +comparison_beq: comparison -> comparison -> bool +bool_beq: bool -> bool -> bool +andb: bool -> bool -> bool +Empty_set_beq: Empty_set -> Empty_set -> 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 +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 diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v new file mode 100644 index 0000000000..f1489f22ae --- /dev/null +++ b/test-suite/output/Search.v @@ -0,0 +1,5 @@ +(* Some tests of the Search command *) + +Search le. (* app nodes *) +Search bool. (* no apps *) +Search (@eq nat). (* complex pattern *) diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out new file mode 100644 index 0000000000..0c32f8d8d9 --- /dev/null +++ b/test-suite/output/SearchPattern.out @@ -0,0 +1,48 @@ +false: bool +true: bool +sumor_beq: + forall (A : Type) (B : Prop), + (A -> A -> bool) -> (B -> B -> bool) -> A + {B} -> A + {B} -> bool +sumbool_beq: + forall A B : Prop, + (A -> A -> bool) -> (B -> B -> bool) -> {A} + {B} -> {A} + {B} -> bool +xorb: bool -> bool -> bool +sum_beq: + forall A B : Type, + (A -> A -> bool) -> (B -> B -> bool) -> A + B -> A + B -> bool +prod_beq: + forall A B : Type, + (A -> A -> bool) -> (B -> B -> bool) -> A * B -> A * B -> bool +orb: bool -> bool -> bool +option_beq: forall A : Type, (A -> A -> bool) -> option A -> option A -> bool +negb: bool -> bool +nat_beq: nat -> nat -> bool +list_beq: forall A : Type, (A -> A -> bool) -> list A -> list A -> bool +implb: bool -> bool -> bool +comparison_beq: comparison -> comparison -> bool +bool_beq: bool -> bool -> bool +andb: bool -> bool -> bool +Empty_set_beq: Empty_set -> Empty_set -> bool +S: nat -> nat +O: 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 +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 +mult_n_Sm: forall n m : nat, n * m + n = n * S m +le_n: forall n : nat, n <= n +eq_refl: forall (A : Type) (x : A), x = x +identity_refl: forall (A : Type) (a : A), identity a a +iff_refl: forall A : Prop, A <-> A +conj: forall A B : Prop, A -> B -> A /\ B +pair: forall A B : Type, A -> B -> A * B diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v new file mode 100644 index 0000000000..802d8c9760 --- /dev/null +++ b/test-suite/output/SearchPattern.v @@ -0,0 +1,19 @@ +(* Some tests of the SearchPattern command *) + +(* Simple, random tests *) +SearchPattern bool. +SearchPattern nat. +SearchPattern le. + +(* With some hypothesis *) +SearchPattern (nat -> nat). +SearchPattern (?n * ?m + ?n = ?n * S ?m). + +(* Non-linearity *) +SearchPattern (_ ?X ?X). + +(* Non-linearity with hypothesis *) +SearchPattern (forall (x:?A) (y:?B), _ ?A ?B). + +(* No delta-reduction *) +SearchPattern (Exc _). diff --git a/test-suite/output/SearchRewrite.out b/test-suite/output/SearchRewrite.out new file mode 100644 index 0000000000..f87aea1c84 --- /dev/null +++ b/test-suite/output/SearchRewrite.out @@ -0,0 +1,2 @@ +plus_n_O: forall n : nat, n = n + 0 +plus_O_n: forall n : nat, 0 + n = n diff --git a/test-suite/output/SearchRewrite.v b/test-suite/output/SearchRewrite.v new file mode 100644 index 0000000000..171a7363fe --- /dev/null +++ b/test-suite/output/SearchRewrite.v @@ -0,0 +1,4 @@ +(* Some tests of the SearchRewrite command *) + +SearchRewrite (_+0). (* left *) +SearchRewrite (0+_). (* right *) |