diff options
Diffstat (limited to 'mathcomp/ssrtest/explain_match.v')
| -rw-r--r-- | mathcomp/ssrtest/explain_match.v | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/mathcomp/ssrtest/explain_match.v b/mathcomp/ssrtest/explain_match.v deleted file mode 100644 index 2c7bc2f..0000000 --- a/mathcomp/ssrtest/explain_match.v +++ /dev/null @@ -1,13 +0,0 @@ -Require Import ssrmatching. -Require Import ssreflect ssrbool ssrnat. - -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. |