blob: 418ece44248c1f8707a82aa09285948b48002d39 (
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
|
Module Type SET.
Axiom T:Set.
Axiom x:T.
End SET.
Implicit Arguments On.
Module M[X:SET].
Definition T := nat.
Definition x := O.
Definition f := [A:Set][x:A]X.x.
End M.
Module N:=M.
Module Nat.
Definition T := nat.
Definition x := O.
End Nat.
Module Z:=(N Nat).
Check (Z.f O).
Module P[Y:SET] := N.
Module Y:=P Z Nat.
Check (Y.f O).
|
