Prototype for LCF-style theorem proving, verified by the compiler and execution-less.
Original (type unsafe) work: https://lara.epfl.ch/w/fv19/labs04
Prototype for LCF-style theorem proving, verified by the compiler and execution-less.
Original (type unsafe) work: https://lara.epfl.ch/w/fv19/labs04