Agda有限集的定義

Question

我是Agda的新手。我正在閱讀Ana Bove和Peter Dybjer的論文「工作中的依賴類型」。我不理解有限集的討論（在我的副本中第15頁）。

本文定義了一個Fin類型：

data Fin : Nat -> Set where 
    fzero : {n : Nat} -> Fin (succ n) 
    fsucc : {n : Nat} -> Fin n -> Fin (succ n) 

我必須失去了一些東西明顯。我不明白這個定義是如何工作的。有人可以簡單地將Fin的定義翻譯成日常英語嗎？這可能是我需要理解本文的這部分內容。

感謝您花時間閱讀我的問題。我很感激。

Answer 1

data Fin : Nat -> Set where 

Fin爲通過自然數參數化數據類型（或：Fin是一種類型的級函數，它接受一個Nat並返回一個Set（基本型），即，對於任意的自然數nFin n是Set ）。

fzero : {n : Nat} -> Fin (succ n) 

對於所有自然數nfzero是該類型的成員/設置Fin (succ n)（從以下，對於所有正數（即除零所有土黃）nfzero是Fin n的成員）。

fsucc : {n : Nat} -> Fin n -> Fin (succ n) 

對於所有自然數n並且所有值Fin n類型的m，fsucc m是Fin (succ n)類型的成員。

---

所以fzero是Fin n對於除零和fsucc m所有n一個構件是Fin n用於表示數比fsucc m更大所有n的部件。

基本上Fin n表示小於n的所有自然數的集合，即對於大小爲n的列表的所有有效索引的集合。