Agdaの有限集合の定義

Question

私はAgdaを初めて使っています。私はAna BoveとPeter Dybjerの論文「Dependent Types at Work」を読んでいます。私は有限集合（15ページの私のコピー）の議論を理解していません。私は何かを明らかに不足しているしなければならない

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

：

紙がFinタイプを定義します。私はこの定義の仕組みを理解していません。誰かが単にFinの定義を毎日の英語に翻訳できますか？これは私がこの論文のこの部分を理解するために必要なものかもしれません。

私の質問を読んでいただきありがとうございます。それは有り難いです。

Answer 1

data Fin : Nat -> Set where 

フィンは、自然数（またはによってパラメータデータタイプである：任意の自然数nFin nため、すなわちNatをとり、Set（基本型）を返すタイプレベル関数は、SetであるFin ）。すべての自然数nfzeroについて

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

タイプのメンバーである/（全ての正の数（ゼロを除く即ち全てナチュラルズ）nfzeroためするFin nのメンバーであることを以下れる）Fin (succ n)セット。すべての自然数n、すべての値型Fin nのmについて

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

は、fsucc m型Fin (succ n)のメンバーです。

---

だからfzeroはゼロとfsucc m除くすべてnためFin nのメンバーがfsucc mより大きい数を表すすべてnためFin nのメンバーです。

基本的にFin nは、nより小さいすべての自然数のセット、つまりサイズnのリストのすべての有効なインデックスを表します。