anchor.diff:  
   and p_letlhs kw (pat, _) =
     (* TODO : this should be refined when head is an applicative pattern (function definition) *)
  -  let pat, ascr_doc =
  +  let pat, ascr =
  +    // if the let binding was written in arrow style, the arguments will be in t
  +    // if it was written in binders style then they will be in pat
       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
  +    | PatAscribed (pat, (t, None)) -> pat, Some (t, empty)
  +    | PatAscribed (pat, (t, Some tac)) -> pat, Some (t, group (str "by" ^^ space ^^ p_atomicTerm tac))
  +    | _ -> pat, None
     in
     match pat.pat with
  -  | PatApp ({pat=PatVar (x, _)}, pats) ->
  +  | PatApp ({pat=PatVar (lid, _)}, pats) ->
         (* has binders *)
  -      prefix2_nonempty (prefix2 (group (kw ^/^ p_lident x)) (flow_map break1 p_atomicPattern pats)) ascr_doc
  +      let ascr_doc =
  +        (match ascr with
  +         | Some (t, tac) -> (sig_as_binders_if_possible t true) ^^ tac
  +         | None -> empty)
  +      in
  +      let bs, style = pats_as_binders_if_possible pats in
  +      let terms = bs @ [ascr_doc] in
  +      group <| kw ^^ space ^^ p_lident lid ^^ (format_sig style terms true)
     | _ ->
         (* doesn't have binders *)
  +      let ascr_doc =
  +        (match ascr with
  +         | Some (t, tac) -> (sig_as_binders_if_possible t false) ^^ tac
  +         | None -> empty)
  +      in
         group (group (kw ^/^ p_tuplePattern pat) ^^ ascr_doc)
   
   and p_letbinding kw (pat, e) =
  
positive.code: // computation type. In case (3), first parameter is indentation for each
  // of the binders, second parameter is indendation for the computation
  // type.
  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
  
  // decide whether a type signature can be printed in the format
  
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
  