anchor.diff:             [ "Int8"; "UInt8"; "Int16"; "UInt16"; "Int32"; "UInt32"; "Int64"; "UInt64"; "UInt128"]
           in
           let int_as_bounded r int_to_t n =
  -            let c = int_as_const r n in
  +            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
  
positive.code:         interpretation=f
      } in
      let unary_int_op (f:int -> int) =
          unary_op arg_as_int (fun r x -> int_as_const 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))
      in
      let unary_bool_op (f:bool -> bool) =
          unary_op arg_as_bool (fun r x -> bool_as_const 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))
      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))
      in
      let list_of_string' rng (s:string) : term =
          let name l = mk (Tm_fvar (lid_as_fv l Delta_constant None)) rng in
  
negative.code:              (PC.op_Subtraction, 2, binary_int_op (fun x y -> (x - y)));
               (PC.op_Multiply,    2, binary_int_op (fun x y -> (Prims.op_Multiply x y)));
               (PC.op_Division,    2, binary_int_op (fun x y -> (x / y)));
               (PC.op_LT,          2, binary_op arg_as_int (fun r x y -> EMB.embed_bool r (x < y)));
               (PC.op_LTE,         2, binary_op arg_as_int (fun r x y -> EMB.embed_bool r (x <= y)));
               (PC.op_GT,          2, binary_op arg_as_int (fun r x y -> EMB.embed_bool r (x > y)));
               (PC.op_GTE,         2, binary_op arg_as_int (fun r x y -> EMB.embed_bool r (x >= y)));
               (PC.op_Modulus,     2, binary_int_op (fun x y -> (x % y)));
               (PC.op_Negation,    1, unary_bool_op (fun x -> not x));
               (PC.op_And,         2, binary_bool_op (fun x y -> x && y));
  