diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/example2.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v index 1856663953..af664ef163 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -157,3 +157,28 @@ intros H. split; fold (1 + 0) (1 + 0) in H. reflexivity. Qed. + +Goal 1 + 1 = 2. +Proof. +cbv [ Nat.add ]. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +let x := reference:(Nat.add) in +cbn beta iota delta [ $x ]. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +simpl beta. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +lazy. +reflexivity. +Qed. |