mini trucs

parent 41b4bbff
......@@ -48,7 +48,7 @@
\end{definition}
\begin{definition}
We define \(\conv_{\beta\Gamma}\) as the reflexive and transitive closure of \(\beta\) and \(\{\mathcal{R} \mid \mathcal{R} \in \Gamma\}\).
We define \(\conv_{\beta\Gamma}\) as the reflexive, symmetric, and transitive closure of \(\beta\) and \(\bigcup_{\mathcal{R} \in \Gamma} \mathcal{R}\).
\end{definition}
\begin{rules}{typing}{Typing rules}
......@@ -111,13 +111,13 @@
{\Gamma \vdash t~u : \subst{B}{x}{u}}
\and
\inferrule{
\Gamma \vdash A : s
\Gamma \vdash t : A
\\
A \conv_{\beta\Gamma} B
\Gamma \vdash B : s
\\
\Gamma \vdash t : A
A \conv_{\beta\Gamma} B
}
{\Gamma \vdash t: B}
\end{rules}
\end{document}
\ No newline at end of file
\end{document}
......@@ -4,11 +4,11 @@
\newcommand{\defn}{\ensuremath{:=}}
\newcommand{\tabs}[3]{\ensuremath{\lambda{#1}~:~{#2}.~{#3}}}
\newcommand{\tabs}[3]{\ensuremath{\lambda{#1}\,{:}\,{#2}.\,{#3}}}
\newcommand{\tapp}[2]{\ensuremath{{#1}~{#2}}}
\newcommand{\tpi}[3]{\ensuremath{\Pi{#1}~:~{#2}.~{#3}}}
\newcommand{\tpi}[3]{\ensuremath{\Pi{#1}\,{:}\,{#2}.\,{#3}}}
\newcommand{\ttype}{\ensuremath{\mathbf{Type}}}
......@@ -38,4 +38,4 @@
\end{mdframed}
\end{figure}
}
\ No newline at end of file
}
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