diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-21 18:20:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-21 18:23:03 +0200 |
| commit | 99efd521c3bd01f885248f6ac03c450e98929b2e (patch) | |
| tree | 0170bfde075802d0206d5b098019e792bbe01cc9 /test-suite/output/Search.out | |
| parent | 783b0af48fc24a2181d960d034d959f265b5d604 (diff) | |
Fixing output test-suite.
Diffstat (limited to 'test-suite/output/Search.out')
| -rw-r--r-- | test-suite/output/Search.out | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 120c6a4ea..dbd72017a 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -1,7 +1,9 @@ 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_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m le_S_n: forall n m : nat, S n <= S m -> n <= m +le_0_n: forall n : nat, 0 <= n +le_n_S: forall n m : nat, n <= m -> S n <= S m true: bool false: bool andb: bool -> bool -> bool @@ -9,9 +11,15 @@ orb: bool -> bool -> bool implb: bool -> bool -> bool xorb: bool -> bool -> bool negb: bool -> bool +Nat.eqb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool +Nat.even: nat -> bool +Nat.odd: nat -> bool +Nat.testbit: nat -> nat -> 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) +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +pred_Sn: forall n : nat, n = Nat.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 @@ -23,7 +31,7 @@ f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 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 +max_l: forall n m : nat, m <= n -> Nat.max n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +min_r: forall n m : nat, m <= n -> Nat.min n m = m |