blob: 27b1fb9f9224e09001cfd30fd47a760ae3c7f1f0 (
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.
|
