diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-04-12 10:08:05 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-15 09:58:47 +0200 |
commit | 15059d887c3059e6d925310be860dd2a3cf97796 (patch) | |
tree | e0c769cbad3b137e738c3e9da766f7f5f5795428 /test-suite/output | |
parent | 3008ce85ed4de549816a1cac4701cb28bee4fad6 (diff) |
[ssr] import ssreflect test suite from math-comp
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/ssr_explain_match.out | 55 | ||||
-rw-r--r-- | test-suite/output/ssr_explain_match.v | 23 |
2 files changed, 78 insertions, 0 deletions
diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out new file mode 100644 index 000000000..fa2393b91 --- /dev/null +++ b/test-suite/output/ssr_explain_match.out @@ -0,0 +1,55 @@ +File "stdin", line 12, characters 0-61: +Warning: Notation _ - _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ <= _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ < _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ >= _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ > _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ <= _ <= _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ < _ <= _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ <= _ < _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ < _ < _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ + _ was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation _ * _ was already used in scope nat_scope. +[notation-overridden,parsing] +BEGIN INSTANCES +instance: (x + y + z) matches: (x + y + z) +instance: (x + y) matches: (x + y) +instance: (x + y) matches: (x + y) +END INSTANCES +BEGIN INSTANCES +instance: (addnC (x + y) z) matches: (x + y + z) +instance: (addnC x y) matches: (x + y) +instance: (addnC x y) matches: (x + y) +END INSTANCES +BEGIN INSTANCES +instance: (addnA x y z) matches: (x + y + z) +END INSTANCES +BEGIN INSTANCES +instance: (addnA x y z) matches: (x + y + z) +instance: (addnC z (x + y)) matches: (x + y + z) +instance: (addnC y x) matches: (x + y) +instance: (addnC y x) matches: (x + y) +END INSTANCES +The command has indeed failed with message: +Ltac call to "ssrinstancesoftpat (cpattern)" failed. +Not supported diff --git a/test-suite/output/ssr_explain_match.v b/test-suite/output/ssr_explain_match.v new file mode 100644 index 000000000..56ca24b6e --- /dev/null +++ b/test-suite/output/ssr_explain_match.v @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import ssrmatching. +Require Import ssreflect ssrbool TestSuite.ssr_mini_mathcomp. + +Definition addnAC := (addnA, addnC). + +Lemma test x y z : x + y + z = x + y. + +ssrinstancesoftpat (_ + _). +ssrinstancesofruleL2R addnC. +ssrinstancesofruleR2L addnA. +ssrinstancesofruleR2L addnAC. +Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *) +Admitted. |