anchor.diff:    let (reqs, enss) = collect_specs false p.pspecs in
     let (rs, es) = (and_of_list reqs, and_of_list enss) in
     ps.PrintLine ("");
  -  (match ps.print_interface with None -> () | Some psi -> psi.PrintLine (""));
     let psi = match ps.print_interface with None -> ps | Some psi -> psi in
     let tactic = match p.pbody with None -> None | Some _ -> attrs_get_exp_opt (Id "tactic") p.pattrs in
     let isPublic = attrs_get_bool (Id "public") false p.pattrs in
  
positive.code:   let isQAttr = attrs_get_bool (Id "qattr") false f.fattrs in
    let isPublicDecl = isPublicDecl || isOpaque in
    let isRecursive = attrs_get_bool (Id "recursive") false f.fattrs in
    (match ps.print_interface with None -> () | Some psi -> psi.PrintLine (""));
    // write everything to *.fsti if it is public and not opaque or publicDecl. 
    // For opaque and publicDecl, only "val" is written into *.fsti if it is public, 
    // everything else goes into *.fst regardless if it is public or not.
  
negative.code:     | (Some _, None) -> ()
      | (_, _) ->
          let psi = if isPublic then psi else ps
          psi.PrintLine ("");
          psi.PrintLine ("val " + (sid p.pname) + " : " + (val_string_of_formals args));
          printPType psi "-> " decreases0
    );
  