| Ian Sweet

| Ian Sweet https://www.impredicative.org PhD Student @ PLUM, University of Maryland, College Park Sun, 19 May 2024 15:53:48 +0000 en-US hourly 1 https://wordpress.org/?v=6.9.4 https://www.impredicative.org/wp-content/uploads/2020/08/cropped-cornifer-1-32x32.png | Ian Sweet https://www.impredicative.org 32 32 An Inference Rule https://www.impredicative.org/2020/08/20/hello-world/ https://www.impredicative.org/2020/08/20/hello-world/#comments Thu, 20 Aug 2020 01:14:21 +0000 http://www.impredicative.org/?p=1 Behold.

\[
\begin{gathered}
{\Gamma \vdash i : \mathbb{Z}}
\qquad
\frac{\Gamma \vdash e_1 : \mathbb{Z} \quad
\Gamma \vdash e_2 : \mathbb{Z}}
{\Gamma \vdash e_1 + e_2 : \mathbb{Z}}
\end{gathered}
\]

Now with code block!

let f (x : int) (y : int) =
  x + y

]]> https://www.impredicative.org/2020/08/20/hello-world/feed/ 1