Examples

tutorial.ipl
A tutorial describing most of the syntactic constructs of IPL.


euler.ipl
A solution to the first Project Euler problem in IPL.


fibonacci.ipl
An implementation of the Fibonacci function, and a solution to the second Project Euler problem.


methcall.ipl
A partial implementation of a problem from the Language Shootout: also demonstrates how classes can be implemented in IPL.


compilation.ipl
Some examples of how high level constructions in type theory are compiled to clean LLVM.


modules.ipl
Describes IPL's approach to modules.


equality.ipl
Describes the difference between definitional and propositional equality.


unary_arithmetic.ipl
Proof assistants often use unary arithmetic: this does not work in IPL as recursive datatypes are not supported. However, unary arithmetic can be approximated using interfaces and procedures.


hedbergs_theorem.ipl
IPL's pedigree includes intuitionistic type theory: some theorems in type theory can be directly implemented in IPL. One prominent example is Hedberg's theorem.