blob: 07a5bc0606f39bde6048d3b6e5997dfabbcd8cfc (
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
|
Module A.
Record Foo := { foo : unit; bar : unit }.
Definition foo_ := {|
foo := tt;
bar := tt
|}.
Definition foo0 (p : Foo) := match p with {| |} => tt end.
Definition foo1 (p : Foo) := match p with {| foo := f |} => f end.
Definition foo2 (p : Foo) := match p with {| foo := f; |} => f end.
Definition foo3 (p : Foo) := match p with {| foo := f; bar := g |} => (f, g) end.
Definition foo4 (p : Foo) := match p with {| foo := f; bar := g; |} => (f, g) end.
End A.
Module B.
Record Foo := { }.
End B.
Module C.
Record Foo := { foo : unit; bar : unit; }.
Definition foo_ := {|
foo := tt;
bar := tt;
|}.
End C.
Module D.
Record Foo := { foo : unit }.
Definition foo_ := {| foo := tt |}.
End D.
Module E.
Record Foo := { foo : unit; }.
Definition foo_ := {| foo := tt; |}.
End E.
Module F.
Record Foo := { foo : nat * nat -> nat -> nat }.
Definition foo_ := {| foo '(x,y) n := x+y+n |}.
End F.
|
