Adding more notations for the lulz.

1 files changed, 16 insertions, 0 deletions

diff --git a/tests/example2.v b/tests/example2.v
index 95485305dc..a7eb02050b 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -192,3 +192,19 @@ unfold &x at 1.
 let x := reference:(Nat.sub) in unfold Nat.add, $x in x.
 reflexivity.
 Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+exists 0, 0; reflexivity.
+Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+eexists _, 0; reflexivity.
+Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+refine '(let x := 0 in _).
+eexists; exists &x; reflexivity.
+Qed.