Extending the toy compiler from Liam O'Connor's blog: Write Your Compiler by Proving It Correct
Original code forked from: https://github.com/liamoc/liamoc.net/blob/master/posts/2015-08-23-verified-compiler.lagda
Syntax and semantics based on the While-int language specification from RSD.