[Added a comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080312211238] hunk ./HuttonsRazor.agda 91
-  -- they don't mention their use of associativity of _◅▻_.
+  -- they don't mention their use of associativity of _◅▻_. (Note that
+  -- a continuation-passing formulation of the compiler would obviate
+  -- the need to prove associativity.)