anchor.diff:                 match x with 
                  | NoSym y -> String "!" <+> (printBoolExprG pVar fr x) |> parened 
                  | _ -> failwith "[printBoolExprG] Grasshopper can't negate spatial things." 
  -           | BEq (x, y) -> infexpr "==" (printExprG pVar fr) [x; y]
  +           | BEq (x, y) -> infexpr "==" (printExprG pVar) [x; y]
  +           | BLt (x, y) -> infexpr "<" (printIntExprG pVar) [x; y]
  +           | BLe (x, y) -> infexpr "<=" (printIntExprG pVar) [x; y]
  +           | BGe (x, y) -> infexpr ">=" (printIntExprG pVar) [x; y]
              | BGt (x, y) -> infexpr ">" (printIntExprG pVar) [x; y]
  -           | BLt (x, y) -> infexpr "<" (printIntExprG pVar) [x; y]
              | _ -> failwith "[printBoolExprG] Case unimplemented for Grasshopper backend."  
          
       /// Pretty-prints an expression.
  
positive.code: 
  open Chessie.ErrorHandling
  
  open Starling 
  open Starling.Collections
  open Starling.Utils
  open Starling.Core.TypeSystem
  open Starling.Core.Var
  open Starling.Core.Expr
  
negative.code:                         |> printBoolExprG (printSymGrass printMarkedVarGrass) true
  
          // TODO @(septract) print command properly 
          let cmdprint =
              let rec matchSymC cmd xs =
                  match cmd with
                  | [] -> Some xs
                  | SymC { Symbol = sym }::cmd' -> matchSymC cmd' (sym::xs)
                  | _ -> None
  
              (* TODO(CaptainHayashi):
                 Currently, the command is not marked with pre-and-post-states.
                 This means that we have to do this marking ourselves, and we 
                 can't easily do this marking soundly with sequential composition.
  
                 For now, we issue a health warning if we spot a sequential
                 composition.  This could do with fixing though... somehow. *)
              let hackilyPrintVarGrass (v : Var) : Doc =
                  printMarkedVarGrass (Before v)
  
              match matchSymC zterm.Original.Cmd.Cmd [] with
              | Some [x] ->
                    printSymbolicGrass (printExprG (printSymGrass hackilyPrintVarGrass)) x
              | Some xs ->
                  vsep
                      [ String "/* WARNING: translation of sequential composition may be unsound. */"
                        (semiSep
                            (List.map
                                (printSymbolicGrass (printExprG (printSymGrass hackilyPrintVarGrass)))
                            xs)) ]
              | None ->
                  // TODO(CaptainHayashi): is this the right fallback?
                  vsep
                      [ String "/* WARNING: Given a non-symbolic command, which is unsupported."
                        String "   Boolean translation is below."
                        Indent
                          (printBoolExprG
                              (printSymGrass printMarkedVarGrass)
                              zterm.SymBool.Cmd)
                        String "   */"
                      ]
          vsep [ String "procedure" <+> String name <+> (varprint |> parened) 
                 String "requires" 
                 Indent wpreprint 
                 String "ensures" 
                 Indent goalprint
                 Indent (braced cmdprint)
               ]  
  
      /// Print all the Grasshopper queries that haven't been eliminated by Z3.      
  