Skip to content
Snippets Groups Projects
Commit fdd2bd19 authored by Ralf Uhlig's avatar Ralf Uhlig
Browse files

fix -->_e

parent 270be84b
No related branches found
No related tags found
No related merge requests found
......@@ -170,9 +170,10 @@ edge [bend left] node {1} (a)
\begin{align*}
(\text{axiom})&\frac{}{\Gamma,x:\alpha\vdash x:\alpha}\\&\\
(\rightarrow_i)&\frac{\Gamma,x:\alpha\vdash t:\beta}{\Gamma\vdash\lambda x.t:\alpha\rightarrow\beta}\\&\\
(\rightarrow_e)&\frac{\Gamma\vdash t:\alpha\rightarrow\beta \qquad\Gamma\vdash t:\alpha}{\Gamma\vdash ts : \beta}\\&\\
(\rightarrow_e)&\frac{\Gamma\vdash t:\alpha\rightarrow\beta \qquad\Gamma\vdash s:\alpha}{\Gamma\vdash ts : \beta}\\&\\
(\forall_i)&\frac{\Gamma\vdash t:\alpha\qquad\text{a} \notin \text{FV}(\Gamma)}{\Gamma\vdash t : \forall \text{a}.\alpha}\\&\\
(\forall_e)&\frac{\Gamma\vdash t :\forall \text{a}.\alpha}{\Gamma\vdash t:(\alpha[\text{a}:=\beta])}\qquad\text{bzw.}\\&\\
(\forall_e)&\frac{\Gamma\vdash t :\forall \text{a}.\alpha}{\Gamma\vdash t\beta:(\alpha[\beta/\text{a}])}\qquad\text{bzw.}\\&\\
(\forall_e)&\frac{}{\Gamma\vdash x:\alpha \left[a_1 \mapsto\beta_1,\ldots,a_k\mapsto\beta_k\right]}(x:\forall a_1 \ldots\forall a_k . \alpha)\in \Gamma\\&\\
(\text{let})&\frac{\Gamma\vdash t:\alpha\qquad\Gamma,x:Cl(\Gamma, \alpha)\vdash s:\beta}{\Gamma\vdash\text{let }x=t\text{ in }s:\beta}
\end{align*}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment