diff options
| author | SimonBoulier | 2020-03-18 11:15:15 +0100 |
|---|---|---|
| committer | SimonBoulier | 2020-03-18 11:15:15 +0100 |
| commit | ea16c402392722a44bf2227aef7ff73faef70d3a (patch) | |
| tree | 6d0373f5e73a235b6e9a348e9b13edd0b76acc8c /test-suite/output/SearchHead.out | |
| parent | 0626df49c72badbb51d2f31eb7d1b1fee22c2638 (diff) | |
Change some ouput tests due to the printing of implicits
Diffstat (limited to 'test-suite/output/SearchHead.out')
| -rw-r--r-- | test-suite/output/SearchHead.out | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 7038eac22c..5627e4bd3c 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -4,6 +4,7 @@ le_S: forall n m : nat, n <= m -> n <= S m le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m le_n_S: forall n m : nat, n <= m -> S n <= S m le_S_n: forall n m : nat, S n <= S m -> n <= m +(use "About" for full details on implicit arguments) false: bool true: bool negb: bool -> bool @@ -17,6 +18,7 @@ Nat.leb: nat -> nat -> bool Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool +(use "About" for full details on implicit arguments) mult_n_O: forall n : nat, 0 = n * 0 plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 @@ -35,5 +37,8 @@ f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 +(use "About" for full details on implicit arguments) h: newdef n +(use "About" for full details on implicit arguments) h: P n +(use "About" for full details on implicit arguments) |