diff options
| author | Hugo Herbelin | 2020-07-28 23:47:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-18 11:28:45 +0100 |
| commit | ca0e42c0ff9e5cebb734bcb59065a4f55ae4aa4e (patch) | |
| tree | 9da6b68e6bd56ced9247ba2135385be8dba86679 /test-suite/output | |
| parent | 396de348a4daa2ae752bed8c75a9ecacb4dcd579 (diff) | |
In recursive notations, accept partial application over the recursive pattern.
This allows e.g. to support a notation of the form "x <== y <== z <= t"
standing for "x <= y /\ y <= z /\ z <= t".
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Notations3.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 10 |
2 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index bd22d45059..623ca316c9 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -249,3 +249,5 @@ myfoo01 tt : nat myfoo01 tt : nat +1 ⪯ 2 ⪯ 3 ⪯ 4 + : Prop diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 839df99ea7..ce97d909a7 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -410,3 +410,13 @@ Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) End Issue8126. + +Module RecursiveNotationPartialApp. + +(* Discussed on Coq Club, 28 July 2020 *) +Notation "x ⪯ y ⪯ .. ⪯ z ⪯ t" := + ((fun b A a => a <= b /\ A b) y .. ((fun b A a => a <= b /\ A b) z (fun b => b <= t)) .. x) + (at level 70, y at next level, z at next level, t at next level). +Check 1 ⪯ 2 ⪯ 3 ⪯ 4. + +End RecursiveNotationPartialApp. |