PrimeImpl.tex

\section{A Prime Implementation of PCF}

In this section, we explore a way of implementing PCF in Idris. 
The use of dependent types in this approach is quite mild, and it should not be too dissimilar to how PCF might be implemented in Haskell.

\input{Lib/PCF/Types}

\input{Lib/PCF/Terms}

\input{Lib/PCF/TypeOf}

\input{Lib/PCF/Substitute}

\input{Lib/PCF/Reduction}