diff options
| author | Enrico Tassi | 2015-03-09 10:43:41 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-12-03 09:50:43 +0100 |
| commit | 55a5aaa22e9dd92ff1c6aba599b878c384c1a66b (patch) | |
| tree | 564600964d90d1ee39fc730f6cb2c5b0086fee15 /mathcomp/ssrtest | |
| parent | de9aafba67f888e1de7921b951d422c864a868a7 (diff) | |
Add commands to trace the matching algorithm
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 |