diff options
Diffstat (limited to 'test-suite/output/Notations3.v')
-rw-r--r-- | test-suite/output/Notations3.v | 62 |
1 files changed, 59 insertions, 3 deletions
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 8c7bbe591..a8d6c97fb 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -59,7 +59,7 @@ Check fun f => CURRYINVLEFT (x:nat) (y:bool), f. (* Notations with variables bound both as a term and as a binder *) (* This is #4592 *) -Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)). +Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope. Check forall n:nat, {# n | 1 > n}. Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop. @@ -183,9 +183,13 @@ Check letpair x [1] = {0}; return (1,2,3,4). (* Test spacing in #5569 *) +Section S1. +Variable plus : nat -> nat -> nat. +Infix "+" := plus. Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). Check 1+1+1. +End S1. (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). @@ -193,7 +197,59 @@ Check !!! (x y:nat), True. (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) -Notation "* x" := (id x) (only printing, at level 15, format "* x"). -Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). +Section S2. +Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope. +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope. Check (((id 1) + 2) + 3). Check (id (1 + 2)). +End S2. + +(* Test printing of notations guided by scope *) + +Module A. + +Delimit Scope line_scope with line. +Notation "{ }" := nil (format "{ }") : line_scope. +Notation "{ x }" := (cons x nil) : line_scope. +Notation "{ x ; y ; .. ; z }" := (cons x (cons y .. (cons z nil) ..)) : line_scope. +Notation "[ ]" := nil (format "[ ]") : matx_scope. +Notation "[ l ]" := (cons l%line nil) : matx_scope. +Notation "[ l ; l' ; .. ; l'' ]" := (cons l%line (cons l'%line .. (cons l''%line nil) ..)) + (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope. + +Open Scope matx_scope. +Check [[0;0]]. +Check [[1;2;3];[4;5;6];[7;8;9]]. + +End A. + +(* Example by Beta Ziliani *) + +Require Import Lists.List. + +Module B. + +Import ListNotations. + +Delimit Scope pattern_scope with pattern. +Delimit Scope patterns_scope with patterns. + +Notation "a => b" := (a, b) (at level 201) : pattern_scope. +Notation "'with' p1 | .. | pn 'end'" := + ((cons p1%pattern (.. (cons pn%pattern nil) ..))) + (at level 91, p1 at level 210, pn at level 210) : patterns_scope. + +Definition mymatch (n:nat) (l : list (nat * nat)) := tt. +Arguments mymatch _ _%patterns. +Notation "'mmatch' n ls" := (mymatch n ls) (at level 0). + +Close Scope patterns_scope. +Close Scope pattern_scope. + +Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end. +Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *) + +Definition alist := [0;1;2]. +Print alist. + +End B. |