blob: fc580f1018078cc9869d97d0c09a6e032d5e4f15 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Module Type ModWithRecord.
Record foo : Type :=
{ A : nat
; B : nat
}.
End ModWithRecord.
Module Test_ModWithRecord (M : ModWithRecord).
Definition test1 : M.foo :=
{| M.A := 0
; M.B := 2
|}.
Module B := M.
Definition test2 : M.foo :=
{| M.A := 0
; M.B := 2
|}.
End Test_ModWithRecord.
|
