Idris, but it's C

A silly experiment where I build a type-safe, HOAS syntax tree for a small C-like language. By way of some syntax extensions, Idris will parse some valid C code into a value which represents the corresponding program.