diff options
| author | Georges Gonthier | 2015-12-04 15:39:27 +0000 |
|---|---|---|
| committer | Georges Gonthier | 2015-12-04 15:39:27 +0000 |
| commit | 672865bc8133d9cd60637f4cf696ed1388166d0a (patch) | |
| tree | dc9998bd97b9555b5fb143be35e17f389263ccb0 /mathcomp/ssrtest/explain_match.v | |
| parent | 732a8c3856f639d723b83fd2e29fe35563120917 (diff) | |
| parent | e6076b24bd95046f82f84c21f205388c17d2e7c8 (diff) | |
Merge branch 'master' of https://github.com/math-comp/math-comp
Diffstat (limited to 'mathcomp/ssrtest/explain_match.v')
| -rw-r--r-- | mathcomp/ssrtest/explain_match.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/mathcomp/ssrtest/explain_match.v b/mathcomp/ssrtest/explain_match.v new file mode 100644 index 0000000..b79453b --- /dev/null +++ b/mathcomp/ssrtest/explain_match.v @@ -0,0 +1,12 @@ +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.
\ No newline at end of file |