diff options
Diffstat (limited to 'tests/example2.v')
| -rw-r--r-- | tests/example2.v | 16 |
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. |