anchor.diff:  let max x y = if x > y then x else y
   
   // VD: copied over from NBE, should both probably go in FStar.List
  -let map_rev (f : 'a -> 'b) (l : list<'a>) : list<'b> =
  +let map_rev (f: 'a -> 'b) (l: list<'a>): list<'b> =
     let rec aux (l:list<'a>) (acc:list<'b>) =
       match l with
       | [] -> acc
       | x :: xs -> aux xs (f x :: acc)
  -  in  aux l []
  -
  +  in
  +  aux l []
  +
  +let rec map_if_all (f: 'a -> option<'b>) (l: list<'a>): option<list<'b>> =
  +  let rec aux l acc =
  +    match l with
  +    | [] -> acc
  +    | x :: xs ->
  +      (match f x with
  +       | Some r -> aux xs (r :: acc)
  +       | None -> [])
  +  in
  +  let r = aux l [] in
  +  if List.length l = List.length r then
  +    Some r
  +  else None
  +
  +let rec all (f: 'a -> bool) (l: list<'a>): bool =
  +  match l with
  +  | [] -> true
  +  | x :: xs -> if f x then all f xs else false
   
   (* [should_print_fs_typ_app] is set when encountering a [LightOff] pragma and *)
   (* reset at the end of each module. If you are using individual print function you *)
  
positive.code: 
  and p_letlhs kw (pat, _) =
    (* TODO : this should be refined when head is an applicative pattern (function definition) *)
    let pat, ascr_doc =
      match pat.pat with
      | PatAscribed (pat, (t, None)) -> pat, group (colon ^^ space ^^ p_tmArrow (Arrows (2, 2)) p_tmNoEq t)
      | PatAscribed (pat, (t, Some tac)) -> pat, group (colon ^^ space ^^ p_tmArrow (Arrows (2, 2)) p_tmNoEq t) ^^ group (str "by" ^^ space ^^ p_atomicTerm tac)
      | _ -> pat, empty
    in
    match pat.pat with
    | PatApp ({pat=PatVar (x, _)}, pats) ->
        (* has binders *)
        prefix2_nonempty (prefix2 (group (kw ^/^ p_lident x)) (flow_map break1 p_atomicPattern pats)) ascr_doc
    | _ ->
        (* doesn't have binders *)
        group (group (kw ^/^ p_tuplePattern pat) ^^ ascr_doc)
  
  and p_letbinding kw (pat, e) =
  
negative.code: // It also needs to make adjustments depending on which style a signature
  // is to be printed in. For more details see the `annotation_style` type
  // definition.
  and format_sig style terms no_last_op =
    let terms', last = List.splitAt (List.length terms - 1) terms in
    let n, last_n, terms', sep, last_op, one_line_space =
      match style with
      | Arrows (n, ln)->
          n, ln, terms', space ^^ rarrow ^^ break1, rarrow ^^ space, space
      | Binders (n, ln, parens) ->
          n, ln,
          (if parens then List.map soft_parens_with_nesting terms' else terms'),
          break1, colon ^^ space,
          (if parens then space else empty)
    in
    let last_op = if List.length terms > 1 && (not no_last_op) then last_op else empty in
    let single_line_arg_indent = repeat n space in
    match List.length terms with
    | 1 -> List.hd terms
    | _ -> group (ifflat (space ^^ (separate sep terms') ^^ one_line_space ^^ last_op ^^ List.hd last)
             (prefix n 1 (group ((ifflat (space ^^ separate sep terms')
               (jump2 ((single_line_arg_indent ^^ separate (sep ^^ single_line_arg_indent) (List.map (fun x -> align (hang 2 x)) terms')))))))
                 (align (hang last_n (last_op ^^ List.hd last)))))
  
  and p_tmArrow style p_Tm e =
    let terms =
      match style with
      | Arrows _ -> p_tmArrow' p_Tm e
      | Binders _ -> collapse_binders p_Tm e
    in
    format_sig style terms false
  
  and p_tmArrow' p_Tm e =
    match e.tm with
  