anchor.diff:  
   (********************************************************************************************************************)
   (* Type-checking a pattern-matching branch                                                                          *)
  +(* scrutinee_expr is the scrutinee expression, used when we also have a returns annotation                          *)
   (* the pattern, when_clause and branch are closed                                                                   *)
   (* scrutinee is the logical name of the expression being matched; it is not in scope in the branch                  *)
  -(*           but it is in scope for the VC of the branch                                                            *)
  +(*   but it is in scope for the VC of the branch                                                                    *)
   (* env does not contain scrutinee, or any of the pattern-bound variables                                            *)
   (* the returned terms are well-formed in an environment extended with the scrutinee only                            *)
   
  
positive.code:         let e = TcUtil.maybe_monadic env e cres.eff_name cres.res_typ in
          //The ascription with the result type is useful for re-checking a term, translating it to Lean etc.
          //AR: revisit, for now doing only if return annotation is not provided
          match ret_or_res_typ with
          | Inr _ -> mk (Tm_ascribed(e, (Inl cres.res_typ, None), Some cres.eff_name)) e.pos
          | Inl _ -> e
        in
  
        //see issue #594: if the scrutinee is impure, then explicitly sequence it with an impure let binding
  
negative.code:        else TcUtil.close_wp_lcomp env pat_bvs c_weak in
  
      c_weak.eff_name,
      Some c_weak.cflags,
      Some maybe_return_c_weak,
      Env.close_guard env binders g_when_weak,
      Env.conj_guard guard_pat g_branch in
  
  