| \(\text{int rule: }\cfrac{}{A,n \Rightarrow n}\qquad\qquad\) | \(\text{true rule: }\cfrac{}{A; true \Rightarrow true}\qquad\qquad\) | \(\text{false rule: }\cfrac{}{A;false \Rightarrow false}\qquad\qquad\) | \(\text{var lookup rule: }\cfrac{A(x)=v}{G, x:v; x\Rightarrow v}\) | ||
| \(\text{if-true rule: }\cfrac{A, e_1\Rightarrow true \qquad A, e_2\Rightarrow v_2}{A; \text{if } e_1 \text{ then } e_2 \text{ else } e_3 \Rightarrow v_2}\qquad\qquad\) | \(\text{if-false rule: }\cfrac{A, e_1\Rightarrow false \qquad A, e_3\Rightarrow v_2}{A; \text{if } e_1 \text{ then } e_2 \text{ else } e_3 \Rightarrow v_2}\qquad\qquad\) | \(\text{let rule: }\cfrac{A; e_1 \Rightarrow v_1 \qquad A, x:v_1; e_2\Rightarrow v_2}{A; \text{let } x = e_1 \text{ in } e_2\Rightarrow v_2}\) | |||
| \(\text{gt rule: }\cfrac{A; e_1\Rightarrow v_1 \qquad A; e_2\Rightarrow v_2 \qquad v_3 \text{ is } v_1 > v_2}{A; e_1 < e_2 \Rightarrow v_3}\qquad\qquad\) | \(\text{lt rule: }\cfrac{A; e_1\Rightarrow v_1 \qquad A; e_2\Rightarrow v_2 \qquad v_3 \text{ is } v_1 < v_2}{A; e_1 < e_2 \Rightarrow v_3}\qquad\qquad\) | ||||
| \(\text{add rule: }\cfrac{A; e_1\Rightarrow v_1 \qquad A; e_2\Rightarrow v_2 \qquad v_3 \text{ is } v_1 + v_2}{A; e_1 + e_2 \Rightarrow v_3}\) | |||||