-T+ while e do s <= T+ e:bool & T+ s
-
-If e is of type bool and s typechecks in context T then the same context is returned
-
-
-
-[SDecl]
-
-T+ t i = e => T,i:t <= i not in T & e:t
-
-if i and e are of the same type and i is not declared in the current scope then i is added with type t to the context.
-
-[SDeclD]
-
-T+ t i => T,i:t <= i not in T
-
-if i is not declared in the current scope, then i is added to the context with type t
-
-[SNoop]
-
-T+ s
-
-SNoops does nothing so the same context is returned
-
-[SPrint]
-
-T+ e <= T+ e:t
+<while e s,c> => c''' => <e,c> => <true,c'> push(c') => c'' <s,c''> => c''', c'''(ret)