Initial commit

1 files changed, 43 insertions, 0 deletions

diff --git a/mathcomp/ssrtest/binders.v b/mathcomp/ssrtest/binders.v
new file mode 100644
index 0000000..6a63167
--- /dev/null
+++ b/mathcomp/ssrtest/binders.v
@@ -0,0 +1,43 @@
+(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+Require Import ssreflect ssrbool eqtype ssrnat.
+
+Lemma test (x : bool) : True.
+have H1 x := x.
+have (x) := x => H2.
+have H3 T (x : T) := x.
+have ? : bool := H1 _ x.
+have ? : bool := H2 _ x.
+have ? : bool := H3 _ x.
+have ? (z : bool) : forall y : bool, z = z := fun y => refl_equal _.
+have ? w : w = w := @refl_equal nat w.
+have ? y : true by [].
+have ? (z : bool) : z = z.
+  exact: (@refl_equal _ z).
+have ? (z w : bool) : z = z by exact: (@refl_equal _ z).
+have H w (a := 3) (_ := 4) : w && true = w.
+  by rewrite andbT.
+exact I.
+Qed.
+
+Lemma test1 : True.
+suff (x : bool): x = x /\ True.
+  by move/(_ true); case=> _.
+split; first by exact: (@refl_equal _ x).
+suff H y : y && true = y /\ True.
+  by case: (H true).
+suff H1 /= : true && true /\ True.
+  by rewrite andbT; split; [exact: (@refl_equal _ y) | exact: I].
+match goal with |- is_true true /\ True => idtac end.
+by split.
+Qed.
+
+Lemma foo n : n >= 0.
+have f i (j := i + n) : j < n.
+  match goal with j := i + n |- _ => idtac end.
+Undo 2.
+suff f i (j := i + n) : j < n.
+  done.
+match goal with j := i + n |- _ => idtac end.
+Undo 3.
+done.
+Qed.