diff options
| author | Hugo Herbelin | 2017-02-16 23:23:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-07 15:18:03 +0200 |
| commit | 495bccc436cfe72af9955b4b9d8564a8831850b9 (patch) | |
| tree | 88820173b82b67f0974108e299615f138a6e8d24 /test-suite | |
| parent | 33f40197e6b7bef02c8df2dc0a0066f8144b66d6 (diff) | |
Fixing #4499 (not using unnamed record field in {| |} notation).
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Record.out | 6 | ||||
| -rw-r--r-- | test-suite/output/Record.v | 5 |
2 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out index 36d643a447..37b4fb25f7 100644 --- a/test-suite/output/Record.out +++ b/test-suite/output/Record.out @@ -14,3 +14,9 @@ build 5 : test_r build_c 5 : test_c +fun '(C _ p) => p + : N -> True +fun '{| T := T |} => T + : N -> Type +fun '(C T p) => (T, p) + : N -> Type * True diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 6aa3df9830..c3d9f1e573 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -19,3 +19,8 @@ Check build 5. Check {| field := 5 |}. Check build_r 5. Check build_c 5. + +Record N := C { T : Type; _ : True }. +Check fun x:N => let 'C _ p := x in p. +Check fun x:N => let 'C T _ := x in T. +Check fun x:N => let 'C T p := x in (T,p). |