diff options
Diffstat (limited to 'mathcomp/ssrtest/elim_pattern.v')
| -rw-r--r-- | mathcomp/ssrtest/elim_pattern.v | 14 |
1 files changed, 14 insertions, 0 deletions
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. + |