Skip to content
Snippets Groups Projects
Commit cf70f15e authored by Michael Sammler's avatar Michael Sammler
Browse files

tweak comment

parent 9016a9b5
No related branches found
No related tags found
No related merge requests found
...@@ -30,15 +30,17 @@ Notation max_list := (max_list_with id). ...@@ -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 (** [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 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 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 := Fixpoint Z_to_little_endian (m : nat) (n : Z) (z : Z) : list Z :=
match m with match m with
| O => [] | O => []
| S m' => Z.land z (Z.ones n) :: Z_to_little_endian m' n (z n) | S m' => Z.land z (Z.ones n) :: Z_to_little_endian m' n (z n)
end. end.
(** [Z_of_little_endian n bs] converts the list [bs] of [n]-bit integers into (** [Z_of_little_endian n bs] converts the list [bs] of [n]-bit integers
a number by interpreting [bs] as the little endian encoding. *) 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 := Fixpoint Z_of_little_endian (n : Z) (bs : list Z) : Z :=
match bs with match bs with
| [] => 0 | [] => 0
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment