필자는 매우 이상한 문법을 보았습니다 : (name : type1) type2는 type이고 expr은 [name : type]입니다. Pi와 Lambda의 대체 구문처럼 보이지만 몇 시간 후에 문서에서 아무 것도 발견하지 못했습니다 검색, 헛된.일부 Coq 이론에서 (a : b) c 및 [a : b] c를 의미하며 정의되는 위치는 무엇입니까?
의미가 무엇이며 어디에 정의되어 있습니까? (죄송합니다. 예제 사용법에 대한 링크를 잃어 버렸습니다)
이전 버전의 Coq. 이 구문은 V8.0을 통해 대대적 인 재 점검을 받았다. V8.0 이론을 V8로 변환하는 툴이 포함 된 V8.0. 이후 릴리스에서 도구가 삭제되었습니다.
Translation from Coq V7 to V8 신문의 변경 사항을 확인할 수 있습니다.
특히, (a:b) c은 보편적 인 정량화이며, 이제는 forall a:b, c; [a:b] c은 람다 추상화로, 이제는 fun a:b => c으로 작성되었습니다. 오래된 이론을 읽을 때 또 다른 중요한 사실은 기능 응용 프로그램에 괄호가 필요하며 우선 순위가 낮다는 것입니다. V7까지는 (f x = y)은 (f (x=y))이고 ([x:nat]y z)은 (([x:nat]y) z)을 의미합니다.
오! 대단히 감사합니다! 나는 이미 그것이 악몽이라고 생각하기 시작했습니다 :) – Vag