Commit 637778a9 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Détails de mise en page

parent 23c38922
......@@ -223,7 +223,9 @@ def sum : (n: Nat) -> F n
\draw[color=red] (-0.8,0.2) to (2,-1.4);
\draw[color=red] (-0.8,-1.4) to (2,0.2);
\item Typing preservation (\emph{Subject reduction}): If a term is well-typed, its reducts have the same type;
\item Confluence: Two reducts of a term have a comon reduct.
......@@ -673,4 +675,6 @@ $\color{red}{(3)}$ append _ (cons x p l) q m
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