forked from GaloisInc/cryptol
-
Notifications
You must be signed in to change notification settings - Fork 0
/
module_system_example.txt
52 lines (33 loc) · 942 Bytes
/
module_system_example.txt
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
signature S where -- u1
type n : # -- u5
module M where -- u2
parameter X : S -- X, u1
-- introduces: u6
-- to do this, we need to resolve `S` first
f : [X.n] -- u7, u6
f = ... -- u7
module N where -- u2
type n = 16 -- u9
module I = -- u4
M with X = N -- u2, X, u3
import I -- u4
-- introduces: u10
g = f -- u8, u10
--------------------------------------------------------------------------------
Defines (naming env)
toplevel:
NS Names Uniq
module S u1
module M u2
module N u3
module I u4
value g u8
u1:
type n u5
u2:
type X.n u6
value f u7
u3:
type n u9
u4:
value f u10