diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-14 13:29:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:04 +0100 |
| commit | 96d6ef7036e19bf1def1512abae5ef8c6ace06b0 (patch) | |
| tree | 2cdbf9f4318d6f6e896cec6f1c401c48e97412e2 /test-suite/output/Notations3.out | |
| parent | a18e87f6a929ce296f8c277b310e286151e06293 (diff) | |
Supporting recursive notations reversing the left-to-right order.
Seizing this opportunity to generalize the possibility for different
associativity into simply reversing the order or not. Also dropping
some dead code.
Example of recursive notation now working:
Notation "[ a , .. , b |- A ]" := (cons b .. (cons a nil) .., A).
Diffstat (limited to 'test-suite/output/Notations3.out')
| -rw-r--r-- | test-suite/output/Notations3.out | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 5bfdec989..58dabe51e 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -173,3 +173,21 @@ exists_true (x : nat) (A : Type) (R : A -> A -> Prop) : Prop * Prop exists_non_null x y z t : nat , x = y /\ z = t : Prop +{{RL 1, 2}} + : nat * (nat * nat) +{{RR 1, 2}} + : nat * nat * nat +@pair nat (prod nat nat) (S (S O)) (@pair nat nat (S O) O) + : prod nat (prod nat nat) +@pair (prod nat nat) nat (@pair nat nat O (S (S O))) (S O) + : prod (prod nat nat) nat +{{RLRR 1, 2}} + : nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) * + (nat * nat * nat) +pair + (pair + (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O))) + (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O))) + : prod + (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat)) + (prod nat (prod nat nat))) (prod (prod nat nat) nat) |