COQ 항목 1.2.10 유형 캐스트 ​​

Question

확실하지 무엇 COQ 매뉴얼 v8.7.0 item 1.2.10에서 다음과 같은 방법 :

• 표현 "용어 : 유형"는 형 캐스트 ​​표현이다. 유형이 유형이되도록합니다.
• "용어 < : 유형는"로컬 용어이 유형 입력이 있는지 확인하기 위해 가상 머신을 설정합니다.

제 생각에는 첫 번째 유형 검사는 Coq (기본값)로 수행되는 반면, 두 번째 검사는 선택된 Coq의 VM (다른 유형 지정 규칙이있을 수 있음)에 의해 수행됩니다. 수도이 기본 및 VM이 같은 동작의 경우 수 :

나는

Check (3 : bool). (* Error: The term "3" has type "nat" while it is expected to have type "bool".*) 
Check (3 <: bool). (* same as above*) 

내 질문이 있다는 것이다 다음 예제를 시도하고 자신의 오류 메시지에서 어떤 차이를 볼 수 없었다?

또한 ":"및 "< :"의 동작이 다르기 때문에 사람들이 다른 하나를 선택하는 데 더주의해야 할 수 있습니다.

Answer 1

내가 아는 한, 기본 감속기구와 VM 감축기구는 동일한 타이핑 규칙을 시행하도록 설계되었습니다.

그러나 일부 계산의 경우 검증 시간은 다른 순서의 차이 일 수 있다는 점에서 동일하게 작동하지 않습니다.

여기 일례 많은 계산이 교정의 중간에서 발생할 수 있기 때문에 이것은 중요한

Time Check (refl_equal 1 : (10^200 - 9 * 10^199)/10^199 = 1). 
... 
Finished transaction in 0.103 secs ... 

Time Check (refl_equal 1 <: (10^200 - 9 * 10^199)/10^199 = 1). 
... 
Finished transaction in 0.053 secs 

이다.