diff options
| -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). |