diff options
| author | Pierre-Marie Pédrot | 2017-08-24 16:48:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-24 17:05:21 +0200 |
| commit | 3cb2f4901ea4d79ff20b45bc4d1968ada1695d3b (patch) | |
| tree | 019b482289496110cd1676dec2e44d1e39133023 /tests | |
| parent | 4c964aa3ecfbb2f6aa52274545c2e27d7d11e179 (diff) | |
Adding notation for the remaining reduction functions.
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. |