From cf70f15e9c4e92bc413d7a79172c804f7b9ab871 Mon Sep 17 00:00:00 2001 From: Michael Sammler <noreply@sammler.me> Date: Wed, 28 Apr 2021 11:32:28 +0200 Subject: [PATCH] tweak comment --- theories/list_numbers.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/theories/list_numbers.v b/theories/list_numbers.v index 96bd6167..fbf61411 100644 --- a/theories/list_numbers.v +++ b/theories/list_numbers.v @@ -30,15 +30,17 @@ Notation max_list := (max_list_with id). (** [Z_to_little_endian m n z] converts [z] into a list of [m] [n]-bit integers in the little endian format. A negative [z] is encoded using two's-complement. If [z] uses more than [m * n] bits, these additional -bits are discarded (see [Z_of_to_little_endian]). [n] should be non-negative. *) +bits are discarded (see [Z_of_to_little_endian]). [n] should be non-negative. +*) Fixpoint Z_to_little_endian (m : nat) (n : Z) (z : Z) : list Z := match m with | O => [] | S m' => Z.land z (Z.ones n) :: Z_to_little_endian m' n (z ≫ n) end. -(** [Z_of_little_endian n bs] converts the list [bs] of [n]-bit integers into -a number by interpreting [bs] as the little endian encoding. *) +(** [Z_of_little_endian n bs] converts the list [bs] of [n]-bit integers +into a number by interpreting [bs] as the little endian encoding. +The integers [b] in [bs] should be in the range [0 ≤ b < 2 ^ n]. *) Fixpoint Z_of_little_endian (n : Z) (bs : list Z) : Z := match bs with | [] => 0 -- GitLab