Commit 700545bb authored by Robbert Krebbers's avatar Robbert Krebbers

Fix some Coqdoc, e.g. use `[ ]` for code, that I did not see in the review of !62,

parent 3666e81e
Pipeline #15546 passed with stage
in 10 minutes and 31 seconds
...@@ -354,21 +354,23 @@ Section list_set. ...@@ -354,21 +354,23 @@ Section list_set.
end. end.
End list_set. End list_set.
(* These next functions allow to efficiently encode lists of positives (bit strings) (** These next functions allow to efficiently encode lists of positives (bit
into a single positive and go in the other direction as well. This is for strings) into a single positive and go in the other direction as well. This is
example used for the countable instance of lists and in namespaces. for example used for the countable instance of lists and in namespaces.
The main functions are positives_flatten and positives_unflatten. *) The main functions are [positives_flatten] and [positives_unflatten]. *)
Fixpoint positives_flatten_go (xs : list positive) (acc : positive) : positive := Fixpoint positives_flatten_go (xs : list positive) (acc : positive) : positive :=
match xs with match xs with
| [] => acc | [] => acc
| x :: xs => positives_flatten_go xs (acc~1~0 ++ Preverse (Pdup x)) | x :: xs => positives_flatten_go xs (acc~1~0 ++ Preverse (Pdup x))
end. end.
(** Flatten a list of positives into a single positive by (** Flatten a list of positives into a single positive by duplicating the bits
duplicating the bits of each element, so that of each element, so that:
* 0 -> 00
* 1 -> 11 - [0 -> 00]
and then separating each element with 10. *) - [1 -> 11]
and then separating each element with [10]. *)
Definition positives_flatten (xs : list positive) : positive := Definition positives_flatten (xs : list positive) : positive :=
positives_flatten_go xs 1. positives_flatten_go xs 1.
...@@ -386,7 +388,7 @@ Fixpoint positives_unflatten_go ...@@ -386,7 +388,7 @@ Fixpoint positives_unflatten_go
end%positive. end%positive.
(** Unflatten a positive into a list of positives, assuming the encoding (** Unflatten a positive into a list of positives, assuming the encoding
used by positives_flatten. *) used by [positives_flatten]. *)
Definition positives_unflatten (p : positive) : option (list positive) := Definition positives_unflatten (p : positive) : option (list positive) :=
positives_unflatten_go p [] 1. positives_unflatten_go p [] 1.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment