Commit e23cc0c7 authored by Simon Spies's avatar Simon Spies

seqZ comment, 80 char line width

parent a370c21f
......@@ -395,8 +395,10 @@ Definition positives_unflatten (p : positive) : option (list positive) :=
positives_unflatten_go p [] 1.
(** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1] over integers, provided [n >= 0]. If n < 0, then the range is empty. **)
Definition seqZ (m len: Z) : list Z := (λ i: nat, Z.add i m) <$> (seq 0 (Z.to_nat len)).
(** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1]
over integers, provided [n >= 0]. If n < 0, then the range is empty. **)
Definition seqZ (m len: Z) : list Z :=
(λ i: nat, Z.add i m) <$> (seq 0 (Z.to_nat len)).
Arguments seqZ : simpl never.
(** * Basic tactics on lists *)
......
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