????有限序列 seq 已經(jīng)在集合的形式化中初步介紹過了，現(xiàn)在我們引入更多的內(nèi)容。

????對于任意的有限序列，我們都可以用一個自然數(shù)表示它的長度（代碼中的 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（將一個有限序列轉(zhuǎn)化為一個集合） 有以下性質(zhì)：

????給定一個二元運算和一個有限序列，我們可以讓這個有限序列中所有的元素都參與這個運算，得到一個最終的運算結(jié)果。這就是大型運算符（）的基礎(chǔ)，具體細節(jié)如下：

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

????seqop 作用在自然數(shù)的有限序列上，有以下實例：

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

????以下代碼中，Ncseq a b 表示從 a 開始遞增且長度為 b 的自然數(shù)的有限序列，Ncoseq a b 表示從 a 開始遞增直到達到?b（不含 b）的自然數(shù)的有限序列。

????有限序列和（無限）序列（類型為 nat -> A 的對象）可以（不完全地）互相轉(zhuǎn)化：

????對于自然數(shù) n 和 a，n 可以被展開為一個序列，其中的每一項都小于 a（a <>?0 時），這就是 n 的?a 進制展開（代碼中的 進制digit）。將展開結(jié)果的每一位乘相應(yīng)權(quán)重后加起來，就能得到原數(shù) n。

????自然數(shù)在某進制下的各位數(shù)字可以用一個有限序列表示（代碼中的 進制nts），在非一進制的情況下這與?進制digit?是一致的。