diff options
Diffstat (limited to 'mathcomp/ssrtest/gen_pattern.v')
| -rw-r--r-- | mathcomp/ssrtest/gen_pattern.v | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/mathcomp/ssrtest/gen_pattern.v b/mathcomp/ssrtest/gen_pattern.v deleted file mode 100644 index eb4aee8..0000000 --- a/mathcomp/ssrtest/gen_pattern.v +++ /dev/null @@ -1,24 +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 ssrnat. - -Notation "( a 'in' c )" := (a + c) (only parsing) : myscope. -Delimit Scope myscope with myscope. - -Notation "( a 'in' c )" := (a + c) (only parsing). - -Lemma foo x y : x + x.+1 = x.+1 + y. -move: {x} (x.+1) {1}x y (x.+1 in RHS). - match goal with |- forall a b c d, b + a = d + c => idtac end. -Admitted. - -Lemma bar x y : x + x.+1 = x.+1 + y. -move E: ((x.+1 in y)) => w. - match goal with |- x + x.+1 = w => rewrite -{w}E end. -move E: (x.+1 in y)%myscope => w. - match goal with |- x + x.+1 = w => rewrite -{w}E end. -move E: ((x + y).+1 as RHS) => w. - match goal with |- x + x.+1 = w => rewrite -{}E -addSn end. -Admitted.
\ No newline at end of file |