diff options
| author | Pierre-Marie Pédrot | 2017-08-25 18:06:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-25 18:40:44 +0200 |
| commit | b3471b2bf449041b47c19e8e12249e4bb36af3ec (patch) | |
| tree | bb288e4e452eba1cf7295cdab900d9164d751058 /tests/example2.v | |
| parent | 8e6338d862873d7e377f59664bbd89e16c0a7309 (diff) | |
Adding more notations for the lulz.
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. |