diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-23 07:39:28 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-23 07:39:28 +0000 |
commit | 9936e2ba36e1d16dcee047d34b0c4caf8c377726 (patch) | |
tree | 2d8e43949545cdf48e8727e4b49cf8a5c5ef7234 /test-suite/output | |
parent | 7ed3805888f7bf974b1e984c8315982442da8627 (diff) |
- Correction filtrage des notations impliquant un "match" : la présence
des localisations empêchait toute unification des pattern de filtrage
de réussir.
- Ajout au passage d'unification des pattern modulo alpha.
- Exemples dans Notations.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9163 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/Notations.out | 10 | ||||
-rw-r--r-- | test-suite/output/Notations.v | 14 |
2 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 3ab3de457..d26051758 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -22,3 +22,13 @@ forall n : nat, n = 0 : list nat (1; 2, 4) : nat * nat * nat +Defining 'ifzero' as keyword +ifzero 3 + : bool +Defining 'pred' as keyword +pred 3 + : nat +fun n : nat => pred n + : nat -> nat +fun n : nat => pred n + : nat -> nat diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 4382975e8..5330e145e 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -17,12 +17,16 @@ Check (decomp (true,true) as t, u in (t,u)). (**********************************************************************) (* Behaviour wrt to binding variables (submitted by Roland Zumkeller) *) +Section A. + Notation "! A" := (forall _:nat, A) (at level 60). Check ! (0=0). Check forall n, n=0. Check forall n:nat, 0=0. +End A. + (**********************************************************************) (* Conflict between notation and notation below coercions *) @@ -66,3 +70,13 @@ 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). + +Notation "'ifzero' n" := (match n with 0 => true | S _ => false end) + (at level 0, n at level 0). +Check (ifzero 3). + +Notation "'pred' n" := (match n with 0 => 0 | S n' => n' end) + (at level 0, n at level 0). +Check (pred 3). +Check (fun n => match n with 0 => 0 | S n => n end). +Check (fun n => match n with S p as x => p | y => 0 end). |