diff options
| author | herbelin | 2006-10-09 17:49:04 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-09 17:49:04 +0000 |
| commit | 01b2d0806c64d77917b82930615057b8586a00fc (patch) | |
| tree | 7b3ad78feac1347fe594f34f6fe155f29aa4f9e7 | |
| parent | 060efb7940d6bea8cb72659e6d16c65443f2e1e7 (diff) | |
Exemple avec liaison des variables de filtrage du match
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9228 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/output/Notations.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations.v | 8 |
2 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 975e2ffdf5..be4cd4faea 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -38,6 +38,10 @@ fun n : nat => pred n : nat -> nat fun n : nat => pred n : nat -> nat +Defining 'ifn' as keyword +Defining 'is' as keyword +fun x : nat => ifn x is succ n then n else 0 + : nat -> nat 1- : bool -4 diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 1d24e70a1e..3cc0a189d0 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -90,6 +90,8 @@ Check (1;2,4). (* Check basic notations involving "match" *) +Section C. + Notation "'ifzero' n" := (match n with 0 => true | S _ => false end) (at level 0, n at level 0). Check (ifzero 3). @@ -100,6 +102,12 @@ 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). +Notation "'ifn' x 'is' 'succ' n 'then' t 'else' u" := + (match x with O => u | S n => t end) (at level 0, u at level 0). +Check fun x => ifn x is succ n then n else 0. + +End C. + (* Check correction of bug #1179 *) Notation "1 -" := true (at level 0). |