diff options
| author | Pierre Courtieu | 2014-12-15 13:51:30 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2014-12-15 13:52:25 +0100 |
| commit | 70819fdda615b9bb1e897bc82c0ce39b28a2dece (patch) | |
| tree | 1a604218ea29640de42d6cb020517cfb6424d8a8 /test-suite/output/SearchPattern.out | |
| parent | 3a83f8aeeff3a4ce13c21045536e17ebb7f96677 (diff) | |
Tests for Searchxxx commands added and modified.
Diffstat (limited to 'test-suite/output/SearchPattern.out')
| -rw-r--r-- | test-suite/output/SearchPattern.out | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 74bbf6882e..1eb7eca8f1 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -75,3 +75,9 @@ pair: forall A B : Type, A -> B -> A * B conj: forall A B : Prop, A -> B -> A /\ B Nat.divmod: nat -> nat -> nat -> nat -> nat * nat +h: n <> newdef n +h: n <> newdef n +h: P n +h': ~ P n +h: P n +h: P n |