🍃 Int32.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Definition t : Set := Z.
Definition zero : t := 0.
Definition one : t := 1.
Definition minus_one : t := -1.
Definition neg (a : t) : t := Pervasives.normalize_int32 (-a).
Definition add (a : t) (b : t) : t := Pervasives.normalize_int32 (Z.add a b).
Definition sub (a : t) (b : t) : t := Pervasives.normalize_int32 (Z.sub a b).
Definition mul (a : t) (b : t) : t := Pervasives.normalize_int32 (Z.mul a b).
Definition div (a : t) (b : t) : t := Pervasives.normalize_int32 (Z.quot a b).
Definition rem (a : t) (b : t) : t := Pervasives.normalize_int32 (Z.rem a b).
Definition succ (a : t) : t := add a 1.
Definition pred (a : t) : t := sub a 1.
Definition abs (a : t) : t := Pervasives.normalize_int32 (Z.abs a).
Definition max_int := 2147483647.
Definition min_int := -2147483648.
Parameter logand : int32 → int32 → int32.
Parameter logor : int32 → int32 → int32.
Parameter logxor : int32 → int32 → int32.
Parameter lognot : int32 → int32.
Parameter shift_left : int32 → int → int32.
Parameter shift_right : int32 → int → int32.
Parameter shift_right_logical : int32 → int → int32.
Definition of_int (a : int) : t := Pervasives.normalize_int32 a.
Definition to_int (a : t) : int := a.
Parameter of_string_opt : string → option t.
Parameter to_string : t → string.
Definition compare (a b : t) : int :=
if a <? b then
-1
else if a =? b then
0
else
1.
Definition equal : t → t → bool := Z.eqb.
Module Notations.
Infix "+i32" := add (at level 50, left associativity).
Infix "-i32" := sub (at level 50, left associativity).
Infix "*i32" := mul (at level 40, left associativity).
Infix "/i32" := div (at level 40, left associativity).
End Notations.
Global Hint Unfold
zero
one
minus_one
neg
add
sub
mul
div
rem
succ
pred
abs
max_int
min_int
of_int
to_int
compare
equal
: tezos_z.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Definition t : Set := Z.
Definition zero : t := 0.
Definition one : t := 1.
Definition minus_one : t := -1.
Definition neg (a : t) : t := Pervasives.normalize_int32 (-a).
Definition add (a : t) (b : t) : t := Pervasives.normalize_int32 (Z.add a b).
Definition sub (a : t) (b : t) : t := Pervasives.normalize_int32 (Z.sub a b).
Definition mul (a : t) (b : t) : t := Pervasives.normalize_int32 (Z.mul a b).
Definition div (a : t) (b : t) : t := Pervasives.normalize_int32 (Z.quot a b).
Definition rem (a : t) (b : t) : t := Pervasives.normalize_int32 (Z.rem a b).
Definition succ (a : t) : t := add a 1.
Definition pred (a : t) : t := sub a 1.
Definition abs (a : t) : t := Pervasives.normalize_int32 (Z.abs a).
Definition max_int := 2147483647.
Definition min_int := -2147483648.
Parameter logand : int32 → int32 → int32.
Parameter logor : int32 → int32 → int32.
Parameter logxor : int32 → int32 → int32.
Parameter lognot : int32 → int32.
Parameter shift_left : int32 → int → int32.
Parameter shift_right : int32 → int → int32.
Parameter shift_right_logical : int32 → int → int32.
Definition of_int (a : int) : t := Pervasives.normalize_int32 a.
Definition to_int (a : t) : int := a.
Parameter of_string_opt : string → option t.
Parameter to_string : t → string.
Definition compare (a b : t) : int :=
if a <? b then
-1
else if a =? b then
0
else
1.
Definition equal : t → t → bool := Z.eqb.
Module Notations.
Infix "+i32" := add (at level 50, left associativity).
Infix "-i32" := sub (at level 50, left associativity).
Infix "*i32" := mul (at level 40, left associativity).
Infix "/i32" := div (at level 40, left associativity).
End Notations.
Global Hint Unfold
zero
one
minus_one
neg
add
sub
mul
div
rem
succ
pred
abs
max_int
min_int
of_int
to_int
compare
equal
: tezos_z.