diff options
| author | Pierre-Marie Pédrot | 2017-08-02 17:31:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-02 17:51:23 +0200 |
| commit | d755c546a5c260232fd30971bd604b078d0afc18 (patch) | |
| tree | 91c6558476ef24bb8e0176cd34c5f4310193095d /tests | |
| parent | dbbefa2ed1f858c1a6de77672e3e1733ef4c28bf (diff) | |
Properly implementing the notation to easily access hypotheses.
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/example2.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v index 398f33561e..ca9e3dcff5 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -19,3 +19,10 @@ Proof. let myvar := Std.NamedHyp @x in split with (?myvar := 0). split. Qed. + +Goal (forall n : nat, n = 0 -> False) -> True. +Proof. +intros H. +elim &H with 0. +split. +Qed. |