Agda의 한정 세트에 대한 정의

Question

나는 Agda를 처음 사용했습니다. 나는 애나 보브 (Ana Bove)와 피터 다이 바이 (Peter Dybjer)가 쓴 "의존형 (Dependent Types at Work)"논문을 읽었습니다. 필자는 Finite Sets에 대한 논의를 이해하지 못합니다 (제 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 

핀은 자연수로 매개 변수화 된 데이터 유형 (또는 : Fin 모든 자연수 nFin n 위해 즉 Set (기본 타입 Nat 걸리는 리턴 타입 레벨 함수) 인 Set 인). 모든 자연수 nfzero 들어

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

이 유형의 멤버/Fin (succ n)는 (여기서 모든 양수 (영 제외한 즉 모든 원주민) 미국 nfzero가 Fin n의 구성원인지 이하)로 설정. 모든 자연수 n 모든 값 유형의 Fin nm 들어

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

는 fsucc mFin (succ n) 형의 부재이다.

---

그래서 fzero가 제로 fsucc m 제외한 모든 n위한 Fin n의 구성원은 fsucc m보다 큰 수를 나타내는 모든 n위한 Fin n의 부재이다.

기본적 Fin n는 n보다 작은 모든 자연수, 즉 크기 n 목록에 대한 유효한 모든 인덱스의 집합을 나타낸다.