diff options
| author | Pierre-Marie Pédrot | 2020-02-06 12:44:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-06 12:44:17 +0100 |
| commit | 55e04a94e52822700ab7215857209da62ef5d2af (patch) | |
| tree | e6e6820e2cf72e88a01608de63c4754ddb124e28 /test-suite | |
| parent | c2f0b3c6c6942d8821ce05759b6940bd77435602 (diff) | |
| parent | 6363875a682ffa36f1f80fa74314c0b68cb2f065 (diff) | |
Merge PR #10835: Accepting a few more variants of format for recursive notations (+ a fix about locations)
Reviewed-by: ppedrot
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. |