example types
This commit is contained in:
parent
641b6d1870
commit
2a1b1a2ba9
1 changed files with 31 additions and 1 deletions
|
@ -6,7 +6,7 @@
|
||||||
\usepackage{amssymb}
|
\usepackage{amssymb}
|
||||||
\usepackage{amsthm}
|
\usepackage{amsthm}
|
||||||
\usepackage{unicode-math}
|
\usepackage{unicode-math}
|
||||||
\usepackage{bussproofs}
|
\usepackage{ebproof}
|
||||||
|
|
||||||
\usepackage{todonotes}
|
\usepackage{todonotes}
|
||||||
\setuptodonotes{size=\tiny}
|
\setuptodonotes{size=\tiny}
|
||||||
|
@ -19,6 +19,36 @@
|
||||||
\begin{document}
|
\begin{document}
|
||||||
\maketitle
|
\maketitle
|
||||||
|
|
||||||
|
\section{Types}
|
||||||
|
|
||||||
|
\[
|
||||||
|
\begin{prooftree}
|
||||||
|
\infer0{\vdash 0 : \text{Int}}
|
||||||
|
\end{prooftree}
|
||||||
|
\\
|
||||||
|
\begin{prooftree}
|
||||||
|
\hypo{Γ \vdash n : \text{Int}}
|
||||||
|
\hypo{Γ \vdash m : \text{Int}}
|
||||||
|
\infer2{Γ \vdash n \text{ + } m : \text{Int}}
|
||||||
|
\end{prooftree}
|
||||||
|
\\
|
||||||
|
\begin{prooftree}
|
||||||
|
\hypo{Γ \vdash n : \text{Int}}
|
||||||
|
\hypo{Γ \vdash m : \text{Int}}
|
||||||
|
\infer2{Γ \vdash n \text{ * } m : \text{Int}}
|
||||||
|
\end{prooftree}
|
||||||
|
\]
|
||||||
|
|
||||||
|
\[
|
||||||
|
\begin{prooftree}
|
||||||
|
\infer0{\vdash \text{o} : \text{\{\}}}
|
||||||
|
\end{prooftree}
|
||||||
|
\\
|
||||||
|
\begin{prooftree}
|
||||||
|
\hypo{Γ, (T_i : \text{Type})_i^* \vdash v : \{ x_i : T_i \}_i}
|
||||||
|
\hypo{Γ, T : \text{Type} \vdash y : T}
|
||||||
|
\infer2{Γ, (T_i : \text{Type})_i^*, T : \text{Type} \vdash v \text{ // } x_y = y : \{ x_i : T_i \} - x_y \cup \{ x_y : T \}}
|
||||||
|
\end{prooftree}
|
||||||
|
\]
|
||||||
|
|
||||||
\end{document}
|
\end{document}
|
||||||
|
|
Loading…
Reference in a new issue