anchor.diff:            BU.format1 "Sig %s\n" (P.sigelt_to_string s) |> failwith
        )
      | None ->
  -       mkConstruct fvar [] [] (* Zoe : Z and S dataconstructors from the examples are not in the environment *)
  +       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 =
  
positive.code: ﻿#light "off"
  module FStar.TypeChecker.NBE
  open FStar.All
  open FStar
  open FStar.TypeChecker
  open FStar.TypeChecker.Env
  open FStar.Syntax.Syntax
  open FStar.Ident
  
  module S = FStar.Syntax.Syntax
  module SS = FStar.Syntax.Subst
  
negative.code: 
      | Tm_let((true, lbs), body) -> 
        translate env (make_rec_env lbs bs) body (* Danel: storing the rec. def. as F* code wrapped in a thunk *)
  
  (* [readback] creates named binders and not De Bruijn *)
  and readback (env:Env.env) (x:t) : term =
  