diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-17 09:34:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-17 09:37:53 +0200 |
| commit | d17237cfd3a67b9a93de98a23ae29869456d2028 (patch) | |
| tree | 5a323cfed9cee00a8dc23b1fac710bbe408c23aa /test-suite/output/Notations3.out | |
| parent | 91f44b164c5d9fa170a8faa7227aff08c1335861 (diff) | |
Fixing interpretation of notations w/ opposite instances of a recursive pattern.
Diffstat (limited to 'test-suite/output/Notations3.out')
| -rw-r--r-- | test-suite/output/Notations3.out | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index b3d2580ac..823418cc1 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -6,3 +6,14 @@ : nat * nat * (nat * nat) pair (pair O (S (S O))) (pair (S (S O)) O) : prod (prod nat nat) (prod nat nat) +<< 0, 2, 4 >> + : nat * nat * nat * (nat * (nat * nat)) +<< 0, 2, 4 >> + : nat * nat * nat * (nat * (nat * nat)) +(0, 2, 4, (2, (2, 0))) + : nat * nat * nat * (nat * (nat * nat)) +(0, 2, 4, (0, (2, 4))) + : nat * nat * nat * (nat * (nat * nat)) +pair (pair (pair O (S (S O))) (S (S (S (S O))))) + (pair (S (S (S (S O)))) (pair (S (S O)) O)) + : prod (prod (prod nat nat) nat) (prod nat (prod nat nat)) |