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