diff options
Diffstat (limited to 'mathcomp/ssrtest/elim_pattern.v')
| -rw-r--r-- | mathcomp/ssrtest/elim_pattern.v | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/mathcomp/ssrtest/elim_pattern.v b/mathcomp/ssrtest/elim_pattern.v deleted file mode 100644 index 24bd0fb..0000000 --- a/mathcomp/ssrtest/elim_pattern.v +++ /dev/null @@ -1,19 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool eqtype ssrnat. -Axiom daemon : False. Ltac myadmit := case: daemon. - -Lemma test x : (x == x) = (x + x.+1 == 2 * x + 1). -case: (X in _ = X) / eqP => _. -match goal with |- (x == x) = true => myadmit end. -match goal with |- (x == x) = false => myadmit end. -Qed. - -Lemma test1 x : (x == x) = (x + x.+1 == 2 * x + 1). -elim: (x in RHS). -match goal with |- (x == x) = _ => myadmit end. -match goal with |- forall n, (x == x) = _ -> (x == x) = _ => myadmit end. -Qed. - |