Before the big rewrite

1 files changed, 18 insertions, 0 deletions

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
new file mode 100644
index 0000000..dde2856
--- /dev/null
+++ b/sec/compiler.ltx
@@ -0,0 +1,18 @@
+\documentclass[../main.tex]{subfiles}
+
+\begin{document}
+\section{Idris 2 Compiler}%
+\label{sec:compiler}
+
+\TODO{
+  \begin{itemize}
+    \item QTT basics
+    \item intrinsically well-scoped AST
+    \item bidirectional judgement
+    \item well-typed data types
+    \item type checking function
+    \item irrelevant pattern matching
+  \end{itemize}
+}
+
+\end{document}