anchor.diff:          interpretation=f
       } in
       let unary_int_op (f:int -> int) =
  -        unary_op arg_as_int (fun r x -> int_as_const r (f x))
  +        unary_op arg_as_int (fun r x -> EMB.embed_int r (f x))
       in
       let binary_int_op (f:int -> int -> int) =
  -        binary_op arg_as_int (fun r x y -> int_as_const r (f x y))
  +        binary_op arg_as_int (fun r x y -> EMB.embed_int r (f x y))
       in
       let unary_bool_op (f:bool -> bool) =
  -        unary_op arg_as_bool (fun r x -> bool_as_const r (f x))
  +        unary_op arg_as_bool (fun r x -> EMB.embed_bool r (f x))
       in
       let binary_bool_op (f:bool -> bool -> bool) =
  -        binary_op arg_as_bool (fun r x y -> bool_as_const r (f x y))
  +        binary_op arg_as_bool (fun r x y -> EMB.embed_bool r (f x y))
       in
       let binary_string_op (f : string -> string -> string) =
  -        binary_op arg_as_string (fun r x y -> string_as_const r (f x y))
  +        binary_op arg_as_string (fun r x y -> EMB.embed_string r (f x y))
       in
       let list_of_string' rng (s:string) : term =
           let name l = mk (Tm_fvar (lid_as_fv l Delta_constant None)) rng in
  
positive.code:     in
      let string_compare' rng (s1:string) (s2:string) : term =
          let r = String.compare s1 s2 in
          int_as_const rng r
      in
      let string_concat' rng args : option<term> =
          match args with
          | [a1; a2] ->
              begin match arg_as_string a1 with
              | Some s1 ->
                  begin match arg_as_list arg_as_string a2 with
                  | Some s2 ->
                      let r = String.concat s1 s2 in
                      Some (string_as_const rng r)
                  | _ -> None
                  end
              | _ -> None
  
negative.code:            [ "Int8"; "UInt8"; "Int16"; "UInt16"; "Int32"; "UInt32"; "Int64"; "UInt64"; "UInt128"]
          in
          let int_as_bounded r int_to_t n =
              let c = EMB.embed_int r n in
              let int_to_t = S.fv_to_tm int_to_t in
              S.mk_Tm_app int_to_t [S.as_arg c] None r
          in
  