有限序列 seq 已经在集合的形式化中初步介绍过了，现在我们引入更多的内容。

对于任意的有限序列，我们都可以用一个自然数表示它的长度（代码中的 seqlength）。

我们可以将任意两个有限序列连接起来形成一个新的有限序列。代码中将 s 和 t 连接后形成的有限序列记为 s ++ t。例如，[::1;2] ++ [::3;4;5] = [::1;2;3;4;5]。

(资料图片仅供参考)

对于 s : seq A 和 f : A -> B，我们可以将 s 中的每一项 x 都替换为 f x，得到一个新的有限序列（代码中记为 seqmap f s）。

在集合的形式化中定义的 SetL（将一个有限序列转化为一个集合） 有以下性质：

给定一个二元运算和一个有限序列，我们可以让这个有限序列中所有的元素都参与这个运算，得到一个最终的运算结果。这就是大型运算符（）的基础，具体细节如下：

如果 op 用 "+" 表示，有 seqop op a [:: x1; x2; ...; xn] = x1 + (x2 + ... (xn + a) ... )。

seqop 作用在自然数的有限序列上，有以下实例：

对于 s : seq nat，Nseqmax s 为 s 中的最大值，Nseqmin s 为 s 中的最小值，Nseqsum s 为 s 中的所有项之和。若 s 为空，以上三者全部为 0。

以下代码中，Ncseq a b 表示从 a 开始递增且长度为 b 的自然数的有限序列，Ncoseq a b 表示从 a 开始递增直到达到 b（不含 b）的自然数的有限序列。

有限序列和（无限）序列（类型为 nat -> A 的对象）可以（不完全地）互相转化：

对于自然数 n 和 a，n 可以被展开为一个序列，其中的每一项都小于 a（a <> 0 时），这就是 n 的 a 进制展开（代码中的 进制digit）。将展开结果的每一位乘相应权重后加起来，就能得到原数 n。

自然数在某进制下的各位数字可以用一个有限序列表示（代码中的 进制nts），在非一进制的情况下这与 进制digit 是一致的。

关键词：