Conv (p.jasmin.2026.09.0.doc.jasmin.jasmin.Jasmin.Conv)

Sourceval z_of_nat : Datatypes.nat -> Z.t

Sourceval int_of_nat : Datatypes.nat -> int

Sourceval nat_of_int : int -> Datatypes.nat

Sourceval cz_of_int : int -> BinNums.coq_Z

Sourceval int_of_cz : BinNums.coq_Z -> int

Sourceval pos_of_z : Z.t -> BinNums.positive

Sourceval z_of_pos : BinNums.positive -> Z.t

Sourceval cz_of_z : Z.t -> BinNums.coq_Z

Sourceval z_of_cz : BinNums.coq_Z -> Z.t

Sourceval word_of_z : Wsize.wsize -> Z.t -> Word0.word

Sourceval int64_of_z : Z.t -> Word0.word

Sourceval int32_of_z : Z.t -> Word0.word

Sourceval z_of_int256 : Word0.word -> Z.t

Sourceval z_of_int128 : Word0.word -> Z.t

Sourceval z_of_int64 : Word0.word -> Z.t

Sourceval z_of_int32 : Word0.word -> Z.t

Sourceval z_of_int16 : Word0.word -> Z.t

Sourceval z_of_int8 : Word0.word -> Z.t

Sourceval z_of_word : Wsize.wsize -> Word0.word -> Z.t

Sourceval z_unsigned_of_word : Wsize.wsize -> Word0.word -> Z.t

Sourceval cty_of_ty : Prog.ty -> Type.atype

Sourceval ty_of_cty : Type.atype -> Prog.ty

Sourceval cvar_of_var : Prog.var -> Var0.Var.var

Sourceval var_of_cvar : Var0.Var.var -> Prog.var

Sourceval vari_of_cvari : Expr.var_i -> Prog.var Jasmin.Prog.L.located

Sourceval csv_of_sv : Prog.Sv.t -> Var0.SvExtra.Sv.t

Sourceval sv_of_csv : Var0.SvExtra.Sv.t -> Prog.Sv.t

Sourceval lval_of_clval : Expr.lval -> Prog.lval

Sourceval cexpr_of_expr : Prog.expr -> Expr.pexpr

Sourceval expr_of_cexpr : Expr.pexpr -> Prog.expr

val cufdef_of_fdef : 
  (unit, 'asm) Prog.func ->
  Var0.funname * 'asm Expr._ufundef

val fdef_of_cufdef : 
  (Var0.funname * 'asm Expr._ufundef) ->
  (unit, 'asm) Prog.func

Sourceval cuprog_of_prog : (unit, 'asm) Prog.prog -> 'asm Expr._uprog

Sourceval prog_of_cuprog : 'asm Expr._uprog -> (unit, 'asm) Prog.prog

val csfdef_of_fdef : 
  ('info, 'asm) Prog.sfundef ->
  Var0.funname * 'asm Expr._sfundef

val fdef_of_csfdef : 
  (Var0.funname * 'asm Expr._sfundef) ->
  (unit, 'asm) Prog.sfundef

Sourceval prog_of_csprog : 'asm Expr._sprog -> (unit, 'asm) Prog.sprog

val to_array : 
  ?signed:bool ->
  Prog.ty ->
  BinNums.coq_Z ->
  Warray_.WArray.array ->
  Wsize.wsize * Z.t array

val error_of_cerror : 
  (Format.formatter -> Compiler_util.pp_error -> unit) ->
  Compiler_util.pp_error_loc ->
  Utils.hierror

val fresh_var_ident : 
  Wsize.v_kind ->
  IInfo.t ->
  Uint63.t ->
  Jasmin.Prog.Name.t ->
  Type.atype ->
  Prog.var