diff options
| author | Pierre-Marie Pédrot | 2017-08-05 14:46:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-05 15:08:31 +0200 |
| commit | dbaf8dd6b150619ac04b33ae4d581432cb5cefe0 (patch) | |
| tree | ed076a8ff6e12613f714d31f5186bf42751ef52d /tests/example2.v | |
| parent | 1f2de88e09c7bb1c0aa111db0d7d50b83f8a62d4 (diff) | |
More notations for basic tactics.
Diffstat (limited to 'tests/example2.v')
| -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 526cbc39f5..76f069a5ae 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -116,3 +116,10 @@ intros n m He He' He''. rewrite <- &He by Std.assumption (). Control.refine (fun () => &He''). Qed. + +Goal forall n (r := if true then n else 0), r = n. +Proof. +intros n r. +hnf in r. +split. +Qed. |