coq에 대한 아주 기본적인 질문입니다. 다음 두 가지 유도 유형을 어떻게 정의합니까?
다음을 포함하는 유형 1 : o fo, ffo, fffo ... k, sk, ssk, sssk ... 여기서 f는 o에 대한 자연수 인덱스로 특성화 될 수 있습니다.
동일한 내용을 포함하는 유형 2이지만 이제 fsffsk 및 sfsfso와 같은 용어도 사용할 수 있습니다.
첫 번째 유형을 올바르게 이해하면 Coq 표준 라이브러리에 정의 된 더 간단한 유형을 결합하여 표현할 수 있습니다.
Definition t1 : Type := nat + nat.
+유형에 대한 연산자는 두 유형의 분리 된 결합입니다. 아이디어는 inl n공용체의 왼쪽에 삽입 된 요소 fff...o가의 n발생 과 함께 문자열을 나타내는 f반면 inr n, 공용체의 오른쪽에 삽입 된 요소 는의 발생 sss...k과 함께 문자열을 나타냅니다 .ns
두 번째 유형의 패턴을 이해하지 못합니다. 정말로 fsffsk대신 쓰려고 했습니까 fsfsfsk?
이 기사는 인터넷에서 수집됩니다. 재 인쇄 할 때 출처를 알려주십시오.
침해가 발생한 경우 연락 주시기 바랍니다[email protected] 삭제
몇 마디 만하겠습니다