diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Notations3.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 7 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 58dabe51e..9c711ff26 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -191,3 +191,5 @@ pair : prod (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat)) (prod nat (prod nat nat))) (prod (prod nat nat) nat) +fun x : nat => if x is n .+ 1 then n else 1 + : nat -> nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index fd5846e71..d81cc702a 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -326,3 +326,10 @@ Check {{RLRR 1 , 2}}. Unset Printing Notations. Check {{RLRR 1 , 2}}. Set Printing Notations. + +(* Check insensitivity of "match" clauses to order *) + +Notation "'if' t 'is' n .+ 1 'then' p 'else' q" := + (match t with S n => p | 0 => q end) + (at level 200). +Check fun x => if x is n.+1 then n else 1. |