anchor.diff:  let mkAccuMatch (s : t) (c : t -> t) = Accu(Match (s, c), [])
   let mkAccuRec (b:letbinding) (env:list<t>) = Accu(Rec(b, env), [])
   let mkAccTyp (u:universe) = Accu(Type u, [])
  -let mkAccInd (fvar : fv) = Accu(Inductive fvar, [])
   
   let isAccu (trm:t) = 
     match trm with 
  
positive.code:       (match args with 
         | [] -> (S.mk (Tm_fvar fv) None Range.dummyRange)
         | _ -> U.mk_app (S.mk (Tm_fvar fv) None Range.dummyRange) args)
      
      | Accu (Var bv, []) ->
        S.bv_to_name bv
      | Accu (Var bv, ts) ->
  
negative.code: let debug_term (t : term) =
    BU.print1 "%s\n" (P.term_to_string t)
  
  let debug_sigmap (m : BU.smap<sigelt>) =
    BU.smap_fold m (fun k v u -> BU.print2 "%s -> %%s\n" k (P.sigelt_to_string_short v)) ()
  
  type var = bv
  type sort = int
  
  //IN F*: type atom : Type0 =
  type atom = //JUST FSHARP
    | Var of var
    | Type of universe (* Zoe: Not sure why this needs to be an atom, just following the paper *)
    | Match of t * (* the scutinee *)
               (t -> t) (* the closure that pattern matches the scrutiny *) 
    | Rec of letbinding * list<t> (* Danel: This wraps a unary F* rec. def. as a thunk in F# *)
  