From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 test-suite/output/Notations.v | 68 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 68 insertions(+)
 create mode 100644 test-suite/output/Notations.v

(limited to 'test-suite/output/Notations.v')

diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
new file mode 100644
index 00000000..4382975e
--- /dev/null
+++ b/test-suite/output/Notations.v
@@ -0,0 +1,68 @@
+(**********************************************************************)
+(* Notations for if and let (submitted by Roland Zumkeller)           *)
+
+Notation "a ? b ; c" := (if a then b else c) (at level 10).
+
+Check (true ? 0 ; 1).
+Check if true as x return (if x then nat else bool) then 0 else true.
+
+Notation "'proj1' t" := (let (a,_) := t in a) (at level 1).
+
+Check (fun e : nat * nat => proj1 e).
+
+Notation "'decomp' a 'as' x , y 'in' b" := (let (x,y) := a in b) (at level 1).
+
+Check (decomp (true,true) as t, u in (t,u)).
+
+(**********************************************************************)
+(* Behaviour wrt to binding variables (submitted by Roland Zumkeller) *)
+
+Notation "! A" := (forall _:nat, A) (at level 60).
+
+Check ! (0=0).
+Check forall n, n=0.
+Check forall n:nat, 0=0.
+
+(**********************************************************************)
+(* Conflict between notation and notation below coercions             *)
+
+(* Case of a printer conflict *)
+
+Require Import BinInt.
+Coercion Zpos : positive >-> Z.
+Open Scope Z_scope.
+
+  (* Check that (Zpos 3) is better printed by the printer for Z than
+     by the printer for positive *)
+
+Check (3 + Zpos 3).
+
+(* Case of a num printer only below coercion (submitted by Georges Gonthier) *)
+
+Open Scope nat_scope.
+
+Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat).
+Coercion Zpos: nat >-> znat.
+ 
+Delimit Scope znat_scope with znat.
+Open Scope znat_scope.
+ 
+Variable addz : znat -> znat -> znat.
+Notation "z1 + z2" := (addz z1 z2) : znat_scope.
+
+  (* Check that "3+3", where 3 is in nat and the coercion to znat is implicit,
+     is printed the same way, and not "S 2 + S 2" as if numeral printing was 
+     only tested with coercion still present *)
+
+Check (3+3).
+
+(**********************************************************************)
+(* Check recursive notations                                          *)
+ 
+Require Import List.
+Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
+Check [1;2;4].
+  
+Reserved Notation "( x ; y , .. , z )" (at level 0).
+Notation "( x ; y , .. , z )" := (pair .. (pair x y) .. z).
+Check (1;2,4).
-- 
cgit v1.2.3