diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-15 14:55:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:05 +0100 |
| commit | 34cf92821e03a2c6ce64c78c66a00624d0fe9c99 (patch) | |
| tree | 7dc6f685aa30f0b5bb3da704f1d96c7060eb19e5 /test-suite/output | |
| parent | 00bfd6fa443232bc908cfa13553e2fa1cf783ffa (diff) | |
In printing notations with "match", reasoning up to the order of clauses.
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. |