diff options
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. |