Sterling Example: stlc:letPair

File: letPair.sos

[Reduce File] [Raw File]

Module stlc:letPair

Builds on stlc:let
Builds on stlc:pair


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


/*Typing Rule*/
typeOf G T1 pairTy(Ty1)
typeOf (X, Ty1)::(Y, Ty1)::G T2 Ty2
----------------------------------- [T-LetPair]
typeOf G letPair(X, Y, T1, T2) Ty2


/*Projection Rule*/
typeOf G T1 pairTy(Ty)
-------------------------- [Proj-LetPair]
/*G |- let x, y = T1 in T2  ~~>
       let X = T1 in let Y = snd(X) in let X = fst(X) in T2*/
G |{term}- letPair(X, Y, T1, T2) ~~>
           let(X, T1, let(Y, snd(var(X)), let(X, fst(var(X)), T2)))