anchor.diff:  ﻿#light "off"
   module FStar.TypeChecker.NBE
   open FStar.All
  +open FStar.Exn
   open FStar
   open FStar.TypeChecker
   open FStar.TypeChecker.Env
   open FStar.Syntax.Syntax
   open FStar.Ident
  +open FStar.Errors
   
   module S = FStar.Syntax.Syntax
   module SS = FStar.Syntax.Subst
  
positive.code:   in 
    aux lbs lbs bs bs
  
  (* We are not targeting tagless normalization at this point *)
  let rec app (f:t) (x:t) (q:aqual) =
    debug (fun () -> BU.print2 "When creating app: %s applied to %s\n" (t_to_string f) (t_to_string x));
  
negative.code:           BU.format1 "Sig %s\n" (P.sigelt_to_string s) |> failwith
       )
     | None ->
         mkConstruct fvar [] [] (* Zoe : Z and S data constructors from the examples are not in the environment *)
  
  (* translate a let-binding - local or global *)
  and translate_letbinding (env:Env.env) (bs:list<t>) (lb:letbinding) : t =
  