Munching squares: Difference between revisions

Content added Content deleted

Inline

@@ Line 108: / Line 108: @@
           (* Test that the index is not out of bounds high. This could
              be proven without a runtime check, but doing that is left
-             as an exercise for the very, very advanced reader. For
+             as an exercise for an advanced reader. For one thing, you
-             one thing, you will need a more complicated version of
+             will need a more complicated version of lxor. Then you
-             lxor. You will likely want to use an external constraint
+             will need to prove, or provide as an axiom, that the XOR
-             solver, as well, or at least a reasonable set of
+             of two numbers of the same number of significant bits is
-             axioms. *)
+             itself restricted to that number of bits. *)
           val () = assertloc (i < numcolors)