A handwritten example demonstrating the measure problems with mutual-recursion.
Cleaning the example more, still has problems with mutual-recursion.
Added recTopoSort to generate clean mutual-recursion; still working out bugs.
RecTopoSort working, termination proved for simple test, but not factorial or limit.
Got termination working.  Need to correctly insert ensures (see XXX in CPSConvert.hs).
Started on loops.  Opened way for tail-call optimization.
Bugfix to if statements and cps conversion.
Progress on loops.
Created Mira library.
Extracted ExpOp from ACL2ConvertCPS.
Extracted ExpOp from ACL2ConvertRTL.
Created CLL IR.  Moved CPSConvert into Mira.
Removed commented code.
Able to compile loop example, still need to produce recursion for loop.
Move file generation to Mira.  Conditionally adds start wrapper if program contains main.
Fixed printing of CLL.
Added implementation to Intriniscs typeclass.  Doesn't handle rtl implementation yet.
Got rid of intrinsic parameterization.
Bugfixes to cps to acl2 conversion.  Debugging loop termination.
Added measures to IRs.  Got rid of alpha conversion.