Commit a6bba167 authored by François Thiré's avatar François Thiré

Merge branch 'master' of git.lsv.fr:fthire/LFMT

parents fad12c90 c766a3f4
......@@ -35,6 +35,8 @@
We denote \(\mathcal{T}_{\mathcal{X}}\) the free algebra over the terms with variables in \(\mathcal{X}\).
\end{definition}
Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\begin{definition}
We define \(\mathfrak{R}_{\mathcal{X}}\) the set of pairs of terms:
\[\mathfrak{R}_{\mathcal{X}} \defn \{(t,u) \mid t,u \in \mathcal{T}_{\mathcal{X}}\} \]
......@@ -44,6 +46,7 @@
We denote \(Dom(\Gamma)\) the domain of \(\Gamma\) defines as:
\begin{align*}
Dom(\emptyset) &\defn \emptyset \\
Dom(\Gamma , \mathcal{R}) &\defn Dom(\Gamma) \\
Dom(\Gamma , x : A) &\defn Dom(\Gamma) \cup \{x\}
\end{align*}
\end{definition}
......@@ -125,6 +128,7 @@
{\Gamma \vdash t: B}
\end{rules}
\begin{lemma}
For any context \(\Gamma\), if \(\tkind \convbg t\) then \(t = \tkind\).
\end{lemma}
......@@ -142,4 +146,21 @@
Notice that if we want to be pedantic, the proofs above need actually to prove a mutual judgment since the congruence relation and the typing judgements are mutually defined.
% \newpage
% \section{A simple wellformedness condition}
% On could start studying a very simple wellformedness condition.
% \begin{rules}{A (perhaps too) simple rule for relation wellformedness}{Relation WF}
% \inferrule{
% \Gamma \vdash A : \ttype
% \\
% \Gamma \vdash t : A
% \\
% \Gamma \vdash u : A
% }
% {\Gamma \vdash \wf{\{(t,u)\}}}
% \end{rules}
\end{document}
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