Type rules unto coercion now represented in ott

1 files changed, 33 insertions, 0 deletions

diff --git a/language/manual.tex b/language/manual.tex
index d96e7263..5d4b9d6a 100644
--- a/language/manual.tex
+++ b/language/manual.tex
@@ -76,9 +76,42 @@
 \ottbuiltXXinXXtypeXXabbreviations\ottinterrule
 \ottfunctions\ottinterrule
 \ottfunctionsXXwithXXcoercions\ottinterrule}
+\newpage
 
 \section{Sail type system}
 
+\subsection{Internal type syntax}
+
+\ottgrammartabular{
+\ottk\ottinterrule
+\ottt\ottinterrule
+\ottoptx\ottinterrule
+\otttag\ottinterrule
+\ottne\ottinterrule
+\otttXXarg\ottinterrule
+\otttXXargs\ottinterrule
+\ottnec\ottinterrule
+\ottSXXN\ottinterrule
+\ottEXXd\ottinterrule
+\ottkinf\ottinterrule
+\otttid\ottinterrule
+\ottEXXk\ottinterrule
+\otttinf\ottinterrule
+\ottEXXa\ottinterrule
+\ottfieldXXtyps\ottinterrule
+\ottEXXr\ottinterrule
+\ottenumerateXXmap\ottinterrule
+\ottEXXe\ottinterrule
+\ottEXXt\ottinterrule
+\ottts\ottinterrule
+\ottE\ottinterrule
+\ottI\ottinterrule
+\ottformula\ottinterrule}
+
+
+\subsection{ Type relations }
+\ottdefnss
+
 \section{Sail operational semantics \{TODO\}}
 
 \end{document}
\ No newline at end of file