diff options
| author | coqbot-app[bot] | 2020-11-18 13:00:03 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-18 13:00:03 +0000 |
| commit | 4a56d4d90294d3f6128d68d7d1d11e3e27ae8b9a (patch) | |
| tree | 96fbb1236ebb85e3ec1be2f49e0a277e793ce5b4 /test-suite | |
| parent | 73a068c60fcb757d3a07602259196fcd73485c11 (diff) | |
| parent | 18269746e59a5f7a698a68d31635e2b81facf2ab (diff) | |
Merge PR #12765: In recursive notations, accept partial application over the recursive pattern
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: jfehrle
Diffstat (limited to 'test-suite')
| -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. |