짧은 :: "Coq"는 수학 읽기와 쓰기를위한 컴퓨터 프로그램입니다 .
무한 데이터 [1, 2, 3, 4, ...]는 짧은 형태로 기술 될 수 있습니다 .
이것은 "2 = 다음에 1", "3 = 다음에 2"... 때문입니다 .

Short :: "Coq" is computer program to read and write mathematics .
The infinite data [ 1 , 2 , 3 , 4 , ... ] can be described in short form .
This is because "2 = next after 1" , "3 = next after 2" ...

Alt+↑/↓ – move through proof; Alt+→ or Alt+⏎ – go to cursor.
Alt+hover executed sentences to watch intermediate steps.
Hover identifiers in goals to view their types. Alt+hover to view definitions.
Company-coq addon is enabled: it will auto-complete names of tactics and lemmas from the standard library, and also show types of lemmas in the right pane.

"Alt + ↑ / ↓": 증명을 전달하십시오. "Alt + →"또는 "Alt + ⏎": 커서로 이동하십시오.
"Alt +"호버링은 문장을 실행하여 중간 단계를 관찰합니다.
대상에 식별자를 올려 해당 유형을 표시합니다. "Alt +"를 가리키면 정의를 볼 수 있습니다.
"Company-coq"애드온을 활성화하십시오 : 표준 라이브러리의 정책 및 보조 정리 이름을 자동으로 완성하고 오른쪽 창에 부트 유형을 표시하십시오.

From Qoc Require Import Sutalgsuhag . (** 짧은 :: "Coq"는 수학 읽기와 쓰기를위한 컴퓨터 프로그램입니다 . 무한 데이터 [1, 2, 3, 4, ...]는 짧은 형태로 기술 될 수 있습니다 . 이것은 "2 = 다음에 1", "3 = 다음에 2"... 때문입니다 . Short :: "Coq" is computer program to read and write mathematics . The infinite data [ 1 , 2 , 3 , 4 , ... ] can be described in short form . This is because "2 = next after 1" , "3 = next after 2" ... *) 꾸러미 무한'수들 . 유도성 무한'수들 : 종류 := 제로 : 무한'수들 | 다음한 : 무한'수들 -> 무한'수들 . 부분 부분1 . 변수 pOutside : 무한'수들 . 고정점 추가'더 yInside : 무한'수들 := 일치해 yInside 돌아가 무한'수들 대 제로 => pOutside | 다음한 xInside => 다음한 (추가'더 xInside) 끝 . 끝 부분1 . 인쇄해 추가'더 . 논증 논증1 : 기능 ( pOutsideInside : 무한'수들 ) , 추가'더 (다음한 제로) pOutsideInside = 추가'더 pOutsideInside (다음한 제로) . 증명 . 이동해'밖 pOutsideInside. 단순화해 . 제거해 pOutsideInside . - (** pOutsideInside is ( 제로 ) *) 단순화해 . 같은 . - (** pOutsideInside is ( 다음한 qOutsideInside ) *) 이동해'밖 qOutsideInside . 이동해'밖 lemma1_qOutsideInside . 단순화해 . 다시쓰해 lemma1_qOutsideInside . 같은 . 확인 . 끝 무한'수들 . (** ** alt ----------------------------------------------------------------------------- *) Module Type infiniteNumbers . Inductive infiniteNumbers : Type := Zero : infiniteNumbers | NextOne : infiniteNumbers -> infiniteNumbers . Section Section1 . Variable pOutside : infiniteNumbers . Fixpoint addMore yInside : infiniteNumbers := match yInside return infiniteNumbers with Zero => pOutside | NextOne xInside => NextOne (addMore xInside) end . End Section1 . Print addMore . Lemma lemma1 : forall ( pOutsideInside : infiniteNumbers ) , addMore (NextOne Zero) pOutsideInside = addMore pOutsideInside (NextOne Zero) . Proof . intros pOutsideInside. simpl . elim pOutsideInside . - (** pOutsideInside is ( Zero ) *) simpl . reflexivity . - (** pOutsideInside is ( NextOne qOutsideInside ) *) intros qOutsideInside . intros lemma1_qOutsideInside . simpl . rewrite lemma1_qOutsideInside . reflexivity . Qed . End infiniteNumbers .