저는 7 장 – "린에서 증명하는 정리"의 귀납적 유형 을 통해 작업하고 있습니다.
나는의 정의를 작성하는 방법을 알고 싶습니다 따라 더 확장 또는 "원시"형태의 비에 의존하는 제품.
튜토리얼에 제공된 정의가 자동으로 몇 가지 세부 사항을 추론하는 것처럼 보입니다. inductive prod1 (α : Type u) (β : Type v) | mk : α → β → prod1
일부 실험을 통해 세부 사항을 채울 수 있습니다. inductive prod2 (α : Type u) (β : Type v) : Type (max u v) | mk : α → β → prod2
그러나 완전히 확장 된 형태로 정의를 제공하면 Pi 유형을 사용하면 유형 검사에 실패합니다. inductive prod3 : Π (α : Type u) (β : Type v), Type (max u v) | mk : α → β → prod3
작성하는 올바른 방법은 무엇입니까 prod3?
마지막으로, 다음 정의는 prod1and와 동일 합니까? prod2즉, 유형 검사기가 항상 αand에 대한 올바른 유형 유니버스를 유추 할 수 β있습니까?
inductive prod4 (α : Type) (β : Type) | mk : α → β → prod4먼저 유형에 의존하는 것이 없다는 점에 유의하십시오. 종속 제품 은 Pi 유형 자체의 또 다른 이름 일뿐입니다 (인덱싱 된 제품의 일반적인 수학적 표기법에서 파생 된 Pi).
귀하의 prod2유형의 올바른 최대한 명시 적 버전입니다 prod1. 에서는 prod3α와 β를 유도 매개 변수 에서 인덱스 로 변경했는데, 알다시피 우주 관련 이유로 작동하지 않습니다. 일반적으로 인덱스는 섹션 7.7에서와 같이 유도 유형 패밀리를 정의하는 데 사용됩니다.
마지막으로, 원자 Type당신이 사용은 prod4의 약자입니다 Type 1. 를 사용 Type*하여 유니버스 매개 변수를 자동으로 유추 할 수 있습니다 .
이 기사는 인터넷에서 수집됩니다. 재 인쇄 할 때 출처를 알려주십시오.
침해가 발생한 경우 연락 주시기 바랍니다[email protected] 삭제
몇 마디 만하겠습니다