anchor.diff:      | Op({idText = "==>"}, [e1;e2]) -> infix0 (str "==>") (p_tmArrow (Arrows (2, 2)) p_tmFormula e1) (p_tmImplies e2)
       | _ -> p_tmArrow (Arrows (2, 2)) p_tmFormula e
   
  -(* This function is somewhat convoluted because it is used in a few different contexts and it's trying to properly  *)
  -(* indent for each of them. For signatures, it is trying to print the whole arrow on one line. If this fails, it    *)
  -(* tries to print everything except the last term on the same line and push the last term on a new line. If this    *)
  -(* fails, it prints every term on a separate line. This seems consistent with the current style used in most cases. *)
  -(* A trailing space may sometimes be introduced, which we should trim.                                              *)
  +// This function is somewhat convoluted because it is used in a few
  +// different contexts and it is trying to properly indent for each of
  +// them. For signatures, it is trying to print the whole arrow on one
  +// line. If this fails, it tries to print everything except the
  +// computation type on the same line and push the computation type on a
  +// new line. If this fails, it prints every term on a separate line. A
  +// trailing space may sometimes be introduced, which we should trim.
  +// 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 p_tmArrow style p_Tm e =
     let terms = p_tmArrow' p_Tm e in
     let terms', last = List.splitAt (List.length terms - 1) terms in
  
positive.code:      has_fsdoc: bool;
       is_fsdoc: bool} //is a standalone fsdoc
  let dummy_meta = {r = dummyRange; has_qs = false; has_attrs = false; has_fsdoc = false; is_fsdoc = false}
  
  type annotation_style =
    | Binders of int * int // val f (x1:t1) ... (xn:tn) : C
    | Arrows of int * int //  val f : x1:t1 -> ... -> xn:tn -> C
  
  // TODO: rewrite in terms of with_comment_sep
  let with_comment printer tm tmrange origin =
  
negative.code:   match List.length terms with
    | 1 -> List.hd terms
    | _ -> group (ifflat ((separate sep terms') ^^ space ^^ last_op ^^ List.hd last)
             (prefix n 1 (group ((ifflat (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' p_Tm e = match e.tm with
    | Product(bs, tgt) -> (List.map (fun b -> p_binder false b) bs) @ (p_tmArrow' p_Tm tgt)
  