int__Int.ml 1.16 KB
Newer Older
1 2
(* This file has been generated from Why3 theory int.Int *)

3
module BigInt = Why3__BigInt
4

5 6 7
let zero  : Why3__BuiltIn.int = BigInt.zero

let one  : Why3__BuiltIn.int = BigInt.one
8 9

let infix_ls (x: Why3__BuiltIn.int) (x1: Why3__BuiltIn.int) : bool =
10
  BigInt.lt x x1
11 12 13 14 15 16 17 18 19

let infix_gt (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
  infix_ls y x

let infix_lseq (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
  infix_ls x y || (x = y)

let infix_pl (x: Why3__BuiltIn.int) (x1:
  Why3__BuiltIn.int) : Why3__BuiltIn.int =
20
  BigInt.add x x1
21 22

let prefix_mn (x: Why3__BuiltIn.int) : Why3__BuiltIn.int =
23
  BigInt.minus x
24 25 26

let infix_as (x: Why3__BuiltIn.int) (x1:
  Why3__BuiltIn.int) : Why3__BuiltIn.int =
27
  BigInt.mul x x1
28 29 30 31 32 33 34 35

let infix_mn (x: Why3__BuiltIn.int) (y:
  Why3__BuiltIn.int) : Why3__BuiltIn.int = infix_pl x (prefix_mn y)

let infix_gteq (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
  infix_lseq y x

let rec for_loop_to x1 x2 body =
36
  if BigInt.le x1 x2 then begin
37
    body x1;
38
    for_loop_to (BigInt.succ x1) x2 body
39 40 41
  end

let rec for_loop_downto x1 x2 body =
42
  if BigInt.ge x1 x2 then begin
43
    body x1;
44
    for_loop_downto (BigInt.pred x1) x2 body
45 46
  end