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/Notations3.out | |
| parent | 00bfd6fa443232bc908cfa13553e2fa1cf783ffa (diff) | |
In printing notations with "match", reasoning up to the order of clauses.
Diffstat (limited to 'test-suite/output/Notations3.out')
| -rw-r--r-- | test-suite/output/Notations3.out | 2 |
1 files changed, 2 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 |