Commit 6ebc8b45 authored by François Thiré's avatar François Thiré

add context closure

parent 2f996682
......@@ -17,9 +17,10 @@
\textbf{Variables} & \(x,y,z,\dots\) & & \\
\textbf{Sorts} & \(s\) & \(\defn\) & \(\ttype{} ~|~ \tkind\) \\
\textbf{Terms} & \(A,B,t,u\) & \(\defn\) & \(x~|~s~|~\tpi{x}{A}{B} ~|~\tabs{x}{A}{u} ~|~ \tapp{t}{u} \)\\
\textbf{Relations} & \(\mathcal{R}\) & & \\
\textbf{Context} & \(\Gamma\) & \(\defn\) & \(\emptyset~|~\Gamma, x:A~|~\Gamma, \mathcal{R}\)\\
\textbf{Typing Judgment} & & & \(\Gamma \vdash t : A\)\\
\textbf{Typing context well-formed} & & & \(\vdash \wf{\Gamma}\) \\
\textbf{Typing context well-formed} & & & \(\phantom{\Gamma} \vdash \wf{\Gamma}\) \\
\textbf{Relation well-formed} & & & \(\Gamma \vdash \wf{\mathcal{R}}\) \\
\end{tabular}
\caption{\lfmt{}}
......@@ -48,7 +49,7 @@
\end{definition}
\begin{definition}
We define \(\conv_{\beta\Gamma}\) as the reflexive, symmetric, and transitive closure of \(\beta\) and \(\bigcup_{\mathcal{R} \in \Gamma} \mathcal{R}\).
We define \(\conv_{\beta\Gamma}\) as the reflexive, symmetric, transitive closure of \(\beta\) and \(\bigcup_{\mathcal{R} \in \Gamma} \mathcal{R}\) and closed by context.
\end{definition}
\begin{rules}{typing}{Typing rules}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment