Datatype.nat 대 nat?

Question

문제는 유도 성 함수를 Coq에 선언하고 테스트하려고합니다.

다음

Inductive natprod : Type := 
    pair : nat -> nat -> natprod. 

Check pair(3 5). 

오류입니다 : :하지만 내 Check 라인에 오류가 있어요

Error: Illegal application (Non-functional construction): 
The expression "3" of type "Datatypes.nat" 
cannot be applied to the term 
"5" : "Datatypes.nat" 

정말 문제가 무엇인지 이해하지

? Datatype.nat과 nat의 차이점은 무엇입니까?

추신 : 나는 "nat"("유도 성 NAT"라고도 함)에 귀납적 함수를 작성했습니다. 거기에 문제가있을 수 있습니까?

Answer 1

pair은 nat -> nat -> natprod의 기능입니다.

Definition threefive := pair 3 5. 

그래서 유형을 테스트하기 :

Check (pair 3 5). 

nat 및 Datatypes.nat이 같은 유형

그래서 당신이 기능을 응용 프로그램 구문을 사용, 적용합니다. 혼란을 피하기 위해 COQ 단지 특정 메시지에 더 자세한되고있는 (이 알려줍니다 당신이 다른 곳에서 다른 버전을 정의한 경우, "데이터 유형 모듈에 정의 된 NAT"...)

---

그리고 나는 당신이 nat 자신을 정의하기 때문에이 메시지가 나타 났을 것 같아요, 그래서 당신이 할 경우, 당신은 아마 문제가 될 수 있습니다 :

Check (pair 3 5). 

때문에 3, 5하지 만든 nat 유형, Datatypes.nat의 부분입니다.

따라서 자신의 nat 유형의 생성자를 사용해야합니다.