anchor.diff:          |> lift (Set.toSeq) 
           |> returnOrFail
   
  +    /// Print a single Grasshopper query from a ZTerm 
  +    let printZTermGrass (svars : VarMap) 
  +                        (name : string) 
  +                        (zterm: Backends.Z3.Types.ZTerm) : Doc =
   
  -    let printZTermGrass (svars : VarMap) 
  -                   (name : string) 
  -                   (zterm: Backends.Z3.Types.ZTerm) : Doc =
  +        // TODO @(septract) print variable types
           let svarprint = VarMap.toTypedVarSeq svars
                           |> Seq.map printTypedVarGrass 
  -
           let varprint = Seq.map printMarkedVarGrass (findVarsGrass zterm) 
                          |> Seq.append svarprint 
                          |> (fun x -> VSep(x,String ",")) 
                          |> Indent 
  +
  +        // Print the requires / ensures clauses 
           let wpreprint = zterm.SymBool.WPre 
  -                        |> printExprGrass 
  +                        |> printBoolExprG (printSymGrass printMarkedVarGrass) 
           let goalprint = zterm.SymBool.Goal 
  -                        |> printExprGrass 
  +                        |> printBoolExprG (printSymGrass printMarkedVarGrass) 
  +
  +        // TODO @(septract) print command properly 
           let cmdprint = zterm.SymBool.Cmd 
                          |> (Core.Expr.Pretty.printBoolExpr (printSymGrass printMarkedVarGrass))
           vsep [ String "procedure" <+> String name <+> (varprint |> parened) 
  
positive.code: 
  [<AutoOpen>] 
  module Types =
      type GrassModel = Backends.Z3.Types.ZModel // Just piggyback on Z3 model for now.  
      type Error = unit 
  
  module Pretty = 
      open Starling.Core.Pretty
  
negative.code:         | Int name -> String name  
          | Bool name -> String name  
          | _ -> failwith "Unimplemented for Grasshopper backend." 
  
      /// Pretty-prints an arithmetic expression.
      let rec printIntExprG (pVar : 'Var -> Doc) : IntExpr<'Var> -> Doc =
  