An Interface to LFPL Prototype Compiler by Robert Atkey
This frontend has been added to the compiler by Michal Konečnư and corresponds to the typing described in his technical report LFPL with Types for Deep Sharing .
The input syntax is the same as for LFPL. This frontend infers certain assertions about the behaviour of the program and produces a pdf displaying them. When it follows from these assertions that the program would execute correctly, the output code is displayed too.Type a program or start with the examples (insertsort.deel, div23.deel, pathlist.deel, reverse.deel, append.deel) :