diff options
Diffstat (limited to 'mathcomp/ssrtest')
| -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 |