From 55a5aaa22e9dd92ff1c6aba599b878c384c1a66b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 9 Mar 2015 10:43:41 +0100
Subject: Add commands to trace the matching algorithm

---
 mathcomp/ssrtest/explain_match.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 mathcomp/ssrtest/explain_match.v

(limited to 'mathcomp/ssrtest')

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
-- 
cgit v1.2.3