diff options
| author | Hugo Herbelin | 2019-10-06 14:33:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-31 15:31:55 +0100 |
| commit | 6363875a682ffa36f1f80fa74314c0b68cb2f065 (patch) | |
| tree | 8a6f4adbbb00a26dc2f51583319cb3f1145f90f1 /test-suite | |
| parent | 23462f128c08922d93e11d65fffb5dca6691639c (diff) | |
More tolerant in format for recursive notations.
This is probably a bit overkill but users are tempted to experiment
it, so we accept that both ends of a recursive notation are surrounded
with boxes which contain printing hints.
The alternative would have been to forbid the ends of a recursive
notation to be in boxes, but strictly speaking it is a bit more
restricting, even if I don't see a realistic use of the general form.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 8 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 26 |
2 files changed, 34 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 799d310fa7..43f88f42a5 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -63,3 +63,11 @@ fun '{| |} => true : R -> bool b = a : Prop +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 26c7840a16..4de6ce19b4 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -158,3 +158,29 @@ Check b = a. End Test. End L. + +Module M. + +(* Accept boxes around the end variables of a recursive notation (if equal boxes) *) + +Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[v' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +End M. |