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
|
grammar
t :: Tm ::= {{ com terms: }}
| let x = t in t' :: :: Let (+ bind x in t' +) {{ com let binding }}
defns
Jop :: '' ::=
defn
t --> t' :: :: red :: E_ {{ com Evaluation }} by
----------------------------- :: LetV
let x=v1 in t2 --> [x|->v1]t2
t1 --> t1'
---------------------------------- :: Let
let x=t1 in t2 --> let x=t1' in t2
defns
Jtype :: '' ::=
defn
G |- t : T :: :: typing :: T_ {{ com Typing }} by
G |- t1:T1
G,x:T1 |- t2:T2
------------------------ :: Let
G |- let x=t1 in t2 : T2
|
