\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}