File: syntax.sos
[Reduce File] [Raw File]
Module tutorial:let
Builds on tutorial:host
tm ::= ...
| let(string, tm, tm)
--------------------------------------------- [Proj-Let]
|{tm}- let(X, T1, T2) ~~> app(abs(X, T2), T1)
eval T1 T11
----------------------------------- [E-Let-Step]
eval let(X, T1, T2) let(X, T11, T2)
value T1
subst X T1 T2 V
--------------------- [E-Let-Subst]
eval let(X, T1, T2) V
X != Y
subst X R T1 S1
subst X R T2 S2
--------------------------------------- [S-Let-NEq]
subst X R let(Y, T1, T2) let(Y, S1, S2)
subst X R T1 S1
--------------------------------------- [S-Let-Eq]
subst X R let(X, T1, T2) let(X, S1, T2)
closed Vars T1
closed X::Vars T2
-------------------------- [C-Let]
closed Vars let(X, T1, T2)
