wip

Author: 5HT

doc/architecture.pdf

@@ -212,7 +212,6 @@ \subsection{Christine: Full CIC (CwF/CwA) \cite{paulinmohring}}\footnote{\url{ht
  cosmos :=&$\textbf{U}_j$ \\
     var :=&$\textbf{var}\ name$ \\
      pi :=&$\Pi\ name\ E\ E\ |\ \lambda\ name\ E\ E\ |\ E\ E$ \\
-  sigma :=&$\Sigma\ name\ E\ E\ |\ (E,E)\ |\ E.1\ |\ E.2$ \\
      id :=&$\textbf{Id}\ E\ |\ \textbf{ref}\ E\ |\ \textbf{id$_J$}\ E$ \\
     ind :=&$\textbf{inductive}\ name\ \textrm{params}\ \textrm{constrs}\ |\ \textbf{constr}\ i\ \textrm{name}\ \textrm{args}\ |\ \textbf{ind}\ \textrm{name}\ E\ \textrm{args}\ E$ \\
 \end{tabular}