blob: 68eff33a63c87337be0d070025a6ba92d434c3e0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
Module Type SIG.
Axiom A : Set.
Axiom B : Set.
End SIG.
Module M : SIG.
Definition A := nat.
Definition B := nat.
End M.
Module N <: SIG := M.
Module TranspId (X: SIG) <: SIG with Definition A := X.A := X.
Module OpaqueId (X: SIG) : SIG with Definition A := X.A := X.
Module TrM := TranspId M.
Module OpM := OpaqueId M.
Print TrM.A.
Print OpM.A.
Print TrM.B.
Print OpM.B.
|
