anchor.diff:          | _ -> failwith "[printIntExprG] Unimplemented for Grasshopper backend." 
   
       /// Pretty-prints a Boolean expression.
  -    and printBoolExprG (pVar : 'Var -> Doc) : BoolExpr<'Var> -> Doc =
  -        function
  +    and printBoolExprG (pVar : 'Var -> Doc) (b : BoolExpr<'Var>) : Doc =
  +        match b with 
           | BVar c -> pVar c
  -        | BAnd xs -> infexprV "&&" (printBoolExprG pVar) xs
  +        | BAnd xs -> infexprV "&&" (printBoolExprG pVar) xs 
           | BOr xs -> infexprV "||" (printBoolExprG pVar) xs
           | BImplies (x, y) -> infexprV "==>" (printBoolExprG pVar)  [x; y]
           | BNot (BEq (x, y)) -> infexpr "!=" (printExprG pVar) [x; y]
           | BEq (x, y) -> infexpr "==" (printExprG pVar) [x; y]
           | BGt (x, y) -> infexpr ">" (printIntExprG pVar) [x; y]
           | BLt (x, y) -> infexpr "<" (printIntExprG pVar) [x; y]
  -        | _ -> failwith "[printBoolExprG] Unimplemented for Grasshopper backend." 
  -
  +        | _ -> failwith "[printBoolExprG] Unimplemented for Grasshopper backend."  
  +       
       /// Pretty-prints an expression.
       and printExprG (pVar : 'Var -> Doc) : Expr<'Var> -> Doc =
           function
  
positive.code: open Starling.Core.Instantiate
  open Starling.Core.GuardedView
  open Starling.Core.Traversal
  
  [<AutoOpen>] 
  module Types =
  
negative.code:         let cmdprint = zterm.SymBool.Cmd 
                         |> (Core.Expr.Pretty.printBoolExpr (printSymGrass printMarkedVarGrass))
          vsep [ String "procedure" <+> String name <+> (varprint |> parened) 
                 // String "requires" 
                 (printConstrGrass (String "requires ") zterm.SymBool.WPre) 
                 (printConstrGrass (String "ensures  ") zterm.SymBool.Goal) 
                 // String "ensures" 
                 // Indent goalprint <+> String ";" 
                 cmdprint 
                      |> ssurround "/*" "*/" 
                      |> Indent |> braced 
               ]  
  
      /// Print all the Grasshopper queries that haven't been eliminated by Z3.      
      let printQuery (model: GrassModel) : Doc = 
          let fails = extractFailures model 
          Map.toSeq fails 
          |> Seq.map (fun (name,term) -> printZTermGrass model.SharedVars name term) 
          |> vsep
  
  