blob: c3d9f1e573b6d81dcf10aea7f22df89dddd9a5b6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
Record test := build { field : nat }.
Record test_r := build_r { field_r : nat }.
Record test_c := build_c { field_c : nat }.
Add Printing Constructor test_c.
Add Printing Record test_r.
Set Printing Records.
Check build 5.
Check {| field := 5 |}.
Check build_r 5.
Check build_c 5.
Unset Printing Records.
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).
|
