Skip to content

Commit f0fc5fb

Browse files
committed
Add num operations used by Itt_omega
1 parent 70f3815 commit f0fc5fb

File tree

2 files changed

+13
-2
lines changed

2 files changed

+13
-2
lines changed

stdlib/lm_num.ml

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ let one_num = Z.one
5757
let minus_one_num = Z.minus_one
5858

5959
(*
60-
* Catch overflows in addition.
60+
* Arithmetics.
6161
*)
6262
let add_num = Z.add
6363
let sub_num = Z.sub
@@ -70,9 +70,16 @@ let quo_num = div_num
7070
let mod_num = rem_num
7171

7272
(*
73-
* Power.
73+
* Euclidean division and remainder, used by Itt_omega.
7474
*)
75+
let ediv_num = Z.ediv
76+
let erem_num = Z.erem
77+
78+
let gcd_num = Z.gcd
7579

80+
(*
81+
* Power.
82+
*)
7683
let power_num = Z.pow
7784

7885
(*

stdlib/lm_num.mli

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,10 @@ val neg_num : num -> num
5656
val abs_num : num -> num
5757
val power_num : num -> int -> num
5858

59+
val ediv_num : num -> num -> num
60+
val erem_num : num -> num -> num
61+
val gcd_num : num -> num -> num
62+
5963
val succ_num : num -> num
6064
val pred_num : num -> num
6165

0 commit comments

Comments
 (0)