Sterling Example: stlc:let

File: let.sos

[Reduce File] [Raw File]

Module stlc:let

Builds on stlc:host


/*New syntax*/
term ::= ...
       | let(string, term, term)


/*Typing Rule*/
typeOf G T1 Ty1
typeOf (X, Ty1)::G T2 Ty2
---------------------------- [T-Let]
typeOf G let(X, T1, T2) Ty2


/*Projection Rule*/
typeOf G T1 Ty1
------------------------------------------------------ [Proj-Let]
G |{term}- let(X, T1, T2) ~~> app(abs(X, Ty1, T2), T1)