From fc84c27eac260dffd8f2fb1cb56d599f1e3486d9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 9 Mar 2015 11:07:53 +0100
Subject: Initial commit

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

(limited to 'mathcomp/ssrtest/elim_pattern.v')

diff --git a/mathcomp/ssrtest/elim_pattern.v b/mathcomp/ssrtest/elim_pattern.v
new file mode 100644
index 0000000..51ab216
--- /dev/null
+++ b/mathcomp/ssrtest/elim_pattern.v
@@ -0,0 +1,14 @@
+Require Import ssreflect ssrbool eqtype ssrnat.
+
+Lemma test x : (x == x) = (x + x.+1 == 2 * x + 1).
+case: (X in _ = X) / eqP => _.
+match goal with |- (x == x) = true => admit end.
+match goal with |- (x == x) = false => admit end.
+Qed.
+
+Lemma test1 x : (x == x) = (x + x.+1 == 2 * x + 1).
+elim: (x in RHS).
+match goal with |- (x == x) = _ => admit end.
+match goal with |- forall n, (x == x) = _ -> (x == x) = _ => admit end.
+Qed.
+
-- 
cgit v1.2.3