diff options
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). |