From 3cb2f4901ea4d79ff20b45bc4d1968ada1695d3b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Aug 2017 16:48:44 +0200
Subject: Adding notation for the remaining reduction functions.

---
 tests/example2.v | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'tests')

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.
-- 
cgit v1.2.3