From 62ea702ac88c2762a6587b7b7c95f8f917cedd1c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Aug 2017 14:40:08 +0200
Subject: Notations for a few reduction functions.

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

(limited to 'tests')

diff --git a/tests/example2.v b/tests/example2.v
index bfb1b07e7a..1856663953 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -123,3 +123,37 @@ intros n r.
 hnf in r.
 split.
 Qed.
+
+Goal 1 = 0 -> 0 = 0.
+Proof.
+intros H.
+pattern 0 at 1.
+let occ := 2 in pattern 1 at 1, 0 at $occ in H.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+vm_compute.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+native_compute.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2 - 0 -> True.
+Proof.
+intros H.
+vm_compute plus in H.
+reflexivity.
+Qed.
+
+Goal 1 = 0 -> True /\ True.
+Proof.
+intros H.
+split; fold (1 + 0) (1 + 0) in H.
+reflexivity.
+Qed.
-- 
cgit v1.2.3