Add a test to resemble issue #4

tchajed · Jun 19, 2019 · c1cb58c · c1cb58c
1 parent f6fe628
commit c1cb58c
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/src/CancelTests.v b/src/CancelTests.v
@@ -109,6 +109,17 @@ Section Tests.
 
 End Tests.
 
+Module GitHubIssues.
+  Inductive perm := Public | Private.
+  Definition value : Type := perm * nat.
+  Theorem test_issue_4 (F: pred nat value) v v1 v2 :
+    F * 0 |-> (Public, v) * 1 |-> v1 * 2 |-> v2 ===>
+    F * 1 |-> v1 * 2 |-> v2 * 0 |-> (Public, v).
+  Proof.
+    cancel.
+  Qed.
+End GitHubIssues.
+
 Module Demo.
 
   Arguments Atom {A V}.