Commit bfebb1e6 authored by Simon Spies's avatar Simon Spies

Notation in seqZ definition

parent 3d6ed210
Pipeline #17943 failed with stage
in 0 seconds
......@@ -396,7 +396,7 @@ Definition positives_unflatten (p : positive) : option (list positive) :=
(** [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) := (fun x: nat => Z.add x m) <$> (seq 0 (Z.to_nat len)).
Definition seqZ (m len: Z) : list Z := (λ x: nat, Z.add x m) <$> (seq 0 (Z.to_nat len)).
Arguments seqZ : simpl never.
......
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