| \(\text{int rule: }\cfrac{}{G \vdash n : int}\qquad\qquad\) | \(\text{true rule: }\cfrac{}{G \vdash true : bool}\qquad\qquad\) | \(\text{false rule: }\cfrac{}{G \vdash false: bool}\qquad\qquad\) | \(\text{var lookup rule: }\cfrac{G(x)=t}{G, x:t \vdash x:t}\) |
| \(\text{if rule: }\cfrac{G \vdash e_1:bool \qquad G \vdash e_2:t\qquad G \vdash e_3:t}{G \vdash \text{if } e_1 \text{ then } e_2 \text{ else } e_3: t}\qquad\qquad\) | \(\text{let rule: }\cfrac{G \vdash e_1:t_1 \qquad G, x:t_1 \vdash e_2:t_2}{G \vdash \text{let } x = e_1 \text{ in } e_2: t_2}\) | ||
| \(\text{gt rule: }\cfrac{G \vdash e_1:'a \qquad G \vdash e_2:'a \qquad (<):'a \rightarrow 'a\rightarrow bool}{G \vdash e_1 < e_2: bool}\qquad\qquad\) | \(\text{lt rule: }\cfrac{G \vdash e_1:'a \qquad G \vdash e_2:'a \qquad (>):'a \rightarrow 'a\rightarrow bool}{G \vdash e_1 > e_2: bool}\) | ||
| \(\text{add rule: }\cfrac{G \vdash e_1:int \qquad G \vdash e_2:int\qquad (+):int \rightarrow int\rightarrow int}{G \vdash e_1 + e_2: int}\) | |||