From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- test-suite/output/Notations.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) (limited to 'test-suite/output/Notations.v') diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 6e637aca..b37c3638 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -129,3 +129,33 @@ Check Nil. Notation NIL := nil. Check NIL : list nat. + + +(**********************************************************************) +(* Test printing of notation with coercions in scope of a coercion *) + +Open Scope nat_scope. + +Coercion is_true := fun b => b=true. +Coercion of_nat n := match n with 0 => true | _ => false end. +Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10). + +Check (false && I 3)%bool /\ I 6. + +(**********************************************************************) +(* Check notations with several recursive patterns *) + +Open Scope Z_scope. + +Notation "[| x , y , .. , z ; a , b , .. , c |]" := + (pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)). +Check [|1,2,3;4,5,6|]. + +(**********************************************************************) +(* Test recursive notations involving applications *) +(* Caveat: does not work for applied constant because constants are *) +(* classified as notations for the particular constant while this *) +(* generic application notation is classified as generic *) + +Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y). +Check fun f => {| f; 0; 1; 2 |} : Z. -- cgit v1.2.3