blob: 7de1e7d55979fa57b870aca11da6aa15fe92a6b9 (
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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
{| field := 5 |}
: test
{| field := 5 |}
: test
{| field_r := 5 |}
: test_r
build_c 5
: test_c
build 5
: test
build 5
: test
{| field_r := 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
fun '{| q := p |} => p
: M -> True
fun '{| U := T |} => T
: M -> Type
fun '{| U := T; q := p |} => (T, p)
: M -> Type * True
fun '{| U := T; a := a; q := p |} => (T, p, a)
: M -> Type * True * nat
fun '{| U := T; a := a; q := p |} => (T, p, a)
: M -> Type * True * nat
{| a := 0; b := 0 |}
: T
fun '{| |} => 0
: LongModuleName.test -> nat
= {|
a :=
{|
LongModuleName.long_field_name0 := 0;
LongModuleName.long_field_name1 := 1;
LongModuleName.long_field_name2 := 2;
LongModuleName.long_field_name3 := 3
|};
b :=
fun
'{|
LongModuleName.long_field_name0 := a;
LongModuleName.long_field_name1 := b;
LongModuleName.long_field_name2 := c;
LongModuleName.long_field_name3 := d
|} => (a, b, c, d)
|}
: T
= {|
a :=
{|
long_field_name0 := 0;
long_field_name1 := 1;
long_field_name2 := 2;
long_field_name3 := 3
|};
b :=
fun
'{|
long_field_name0 := a;
long_field_name1 := b;
long_field_name2 := c;
long_field_name3 := d
|} => (a, b, c, d)
|}
: T
|
