diff options
| author | Pierre-Marie Pédrot | 2019-11-13 15:20:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-13 15:20:55 +0100 |
| commit | b9def53df5a69d5d4dbf46bd846281220b4fe1db (patch) | |
| tree | 45033df823d49f98485f3eede15c4e89398924cd /test-suite | |
| parent | dde10a9b2512ffc7e941c79bbc442c5b4b1f45f9 (diff) | |
| parent | 1e5bae9d78192e3f0c5d7e25ab7e64fdc605316f (diff) | |
Merge PR #11094: Miscellaneous micro-improvements of the syntax of records
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 7 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index c1b9a2b1c6..ba4ac5a8f9 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -57,3 +57,5 @@ where |- Type] (pat, p0, p cannot be used) ?T0 : [y : nat pat : ?T0 * nat p0 : ?T0 * nat p := p0 : ?T0 * nat |- Type] (pat, p0, p cannot be used) +fun '{| |} => true + : R -> bool diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index d1063bfd04..4b9d0abd95 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -133,3 +133,10 @@ Check fun y : nat => # (x,z) |-> y & y. Check fun y : nat => # (x,z) |-> (x + y) & (y + z). End K. + +Module EmptyRecordSyntax. + +Record R := { n : nat }. +Check fun '{|n:=x|} => true. + +End EmptyRecordSyntax. |