summaryrefslogtreecommitdiff
path: root/kernel/uint31.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /kernel/uint31.mli
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'kernel/uint31.mli')
-rw-r--r--kernel/uint31.mli41
1 files changed, 41 insertions, 0 deletions
diff --git a/kernel/uint31.mli b/kernel/uint31.mli
new file mode 100644
index 00000000..e8b98080
--- /dev/null
+++ b/kernel/uint31.mli
@@ -0,0 +1,41 @@
+type t
+
+ (* conversion to int *)
+val to_int : t -> int
+val of_int : int -> t
+val of_uint : int -> t
+
+ (* convertion to a string *)
+val to_string : t -> string
+val of_string : string -> t
+
+ (* logical operations *)
+val l_sl : t -> t -> t
+val l_sr : t -> t -> t
+val l_and : t -> t -> t
+val l_xor : t -> t -> t
+val l_or : t -> t -> t
+
+ (* Arithmetic operations *)
+val add : t -> t -> t
+val sub : t -> t -> t
+val mul : t -> t -> t
+val div : t -> t -> t
+val rem : t -> t -> t
+
+ (* Specific arithmetic operations *)
+val mulc : t -> t -> t * t
+val div21 : t -> t -> t -> t * t
+
+ (* comparison *)
+val lt : t -> t -> bool
+val equal : t -> t -> bool
+val le : t -> t -> bool
+val compare : t -> t -> int
+
+ (* head and tail *)
+val head0 : t -> t
+val tail0 : t -> t
+
+(** Used by retroknowledge *)
+val add_digit : t -> t -> t