diff options
| author | herbelin | 2006-01-11 19:19:41 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-11 19:19:41 +0000 |
| commit | 83e16708ab8e6a8aaaeb1389be646c28271d40fe (patch) | |
| tree | ee8ee321e922987d4e2ba71d930d34367b4c2fb3 /test-suite | |
| parent | 9d26b73255b86ec710d8a59c8f196f96229b17c9 (diff) | |
Ajout test notation récursive
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7847 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations.v | 11 |
2 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 321c60eb10..3ab3de4571 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -18,3 +18,7 @@ forall n : nat, n = 0 : Z 3 + 3 : znat +[1; 2; 4] + : list nat +(1; 2, 4) + : nat * nat * nat diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index fdce2b2511..4382975e86 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -55,3 +55,14 @@ Notation "z1 + z2" := (addz z1 z2) : znat_scope. 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). |