blob: 1e9273f07c81d5b628f135af22489d750aa1c66d (
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 M.
Definition t:=nat.
Definition x:=O.
End M.
Print M.t.
Module Type SIG.
Parameter t:Set.
Parameter x:t.
End SIG.
Module F[X:SIG].
Definition t:=X.t->X.t.
Definition x:t.
Intro.
Exact X.x.
Defined.
Definition y:=X.x.
End F.
Module N := F M.
Print N.t.
Eval Compute in N.t.
Module N' : SIG := N.
Print N'.t.
Eval Compute in N'.t.
Module N'' <: SIG := F N.
Print N''.t.
Eval Compute in N''.t.
Eval Compute in N''.x.
Module N''' : SIG with Definition t:=nat->nat := N.
Print N'''.t.
Eval Compute in N'''.t.
Print N'''.x.
Import N'''.
Print t.
|
