🍃 Int64.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_int64 (-a).
Definition add (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.add a b).
Definition sub (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.sub a b).
Definition mul (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.mul a b).
Definition div (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.quot a b).
Definition rem (a : t) (b : t) : t := Pervasives.normalize_int64 (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_int64 (Z.abs a).
Definition max_int : t := 9223372036854775807.
Definition min_int : t := -9223372036854775808.
Parameter logand : int64 → int64 → int64.
Parameter logor : int64 → int64 → int64.
Parameter logxor : int64 → int64 → int64.
Parameter lognot : int64 → int64.
Parameter shift_left : int64 → int → int64.
Parameter shift_right : int64 → int → int64.
Parameter shift_right_logical : int64 → int → int64.
Definition of_int (a : int) : t := a.
Definition to_int (a : t) : int := Pervasives.normalize_int a.
Definition of_int32 (a : int32) : t := a.
Definition to_int32 (a : t) : int32 := Pervasives.normalize_int32 a.
Parameter of_string_opt : string → option int64.
Parameter to_string : int64 → 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 "+i64" := add (at level 50, left associativity).
Infix "-i64" := sub (at level 50, left associativity).
Infix "*i64" := mul (at level 40, left associativity).
Infix "/i64" := 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
of_int32
to_int32
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_int64 (-a).
Definition add (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.add a b).
Definition sub (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.sub a b).
Definition mul (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.mul a b).
Definition div (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.quot a b).
Definition rem (a : t) (b : t) : t := Pervasives.normalize_int64 (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_int64 (Z.abs a).
Definition max_int : t := 9223372036854775807.
Definition min_int : t := -9223372036854775808.
Parameter logand : int64 → int64 → int64.
Parameter logor : int64 → int64 → int64.
Parameter logxor : int64 → int64 → int64.
Parameter lognot : int64 → int64.
Parameter shift_left : int64 → int → int64.
Parameter shift_right : int64 → int → int64.
Parameter shift_right_logical : int64 → int → int64.
Definition of_int (a : int) : t := a.
Definition to_int (a : t) : int := Pervasives.normalize_int a.
Definition of_int32 (a : int32) : t := a.
Definition to_int32 (a : t) : int32 := Pervasives.normalize_int32 a.
Parameter of_string_opt : string → option int64.
Parameter to_string : int64 → 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 "+i64" := add (at level 50, left associativity).
Infix "-i64" := sub (at level 50, left associativity).
Infix "*i64" := mul (at level 40, left associativity).
Infix "/i64" := 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
of_int32
to_int32
compare
equal
: tezos_z.