aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules/Demo.v
blob: 1f27fe1ba1ac784338154dedb344993c55b6940a (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 := 0.
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.