diff --git a/LaTeX/lfmt.tex b/LaTeX/lfmt.tex index 0172f2d6aae22261f198f292ebe72cbf68e20801..a7ad5c7cebaed6c294291c6b4245074620429fcd 100644 --- a/LaTeX/lfmt.tex +++ b/LaTeX/lfmt.tex @@ -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} @@ -121,4 +124,23 @@ {\Gamma \vdash t: B} \end{rules} + +\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}