blob: 070f859eaa22e83cbda3e5a936d7c4b8ab7bb322 (
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.
Set Implicit Arguments.
Unset Strict Implicit.
Module M (X: SET).
Definition T := nat.
Definition x := 0.
Definition f (A : Set) (x : A) := X.x.
End M.
Module N := M.
Module Nat.
Definition T := nat.
Definition x := 0.
End Nat.
Module Z := N Nat.
Check (Z.f 0).
Module P (Y: SET) := N.
Module Y := P Z Nat.
Check (Y.f 0).
|
