From ac23ba349a2d3254d21e942e657b02e533e64f9c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?J=C3=A9r=C3=B4me=20Vouillon?= Date: Wed, 25 Oct 2023 12:29:55 +0200 Subject: [PATCH] Implement Nat.length_nat as an external primitive --- src/nat.ml | 2 +- src/nat.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/nat.ml b/src/nat.ml index f52f73c..e8527f7 100644 --- a/src/nat.ml +++ b/src/nat.ml @@ -67,7 +67,7 @@ external lxor_digit_nat: nat -> int -> nat -> int -> unit = "lxor_digit_nat" external initialize_nat: unit -> unit = "initialize_nat" let _ = initialize_nat() -let length_nat (n : nat) = Obj.size (Obj.repr n) - 1 +external length_nat : nat -> int = "length_nat" let length_of_digit = Sys.word_size;; diff --git a/src/nat.mli b/src/nat.mli index 803a653..5c82597 100644 --- a/src/nat.mli +++ b/src/nat.mli @@ -30,7 +30,7 @@ external nth_digit_nat: nat -> int -> int = "nth_digit_nat" external set_digit_nat_native: nat -> int -> nativeint -> unit = "set_digit_nat_native" external nth_digit_nat_native: nat -> int -> nativeint = "nth_digit_nat_native" -val length_nat : nat -> int +external length_nat : nat -> int = "length_nat" external num_digits_nat: nat -> int -> int -> int = "num_digits_nat" external num_leading_zero_bits_in_digit: nat -> int -> int = "num_leading_zero_bits_in_digit"