짧은 ::
(1.) "Coq"는 수학 읽기와 쓰기를위한 컴퓨터 프로그램입니다 .
(2.) 많은 정의 "d"와 보조 표제 "l"을 매개 변수화하는 매개 변수 "p"는 모두 하나에 패키지화 될 수 있습니다.
(3.) 그런 다음 나중에이 매개 변수 "p"가 인스턴스화되어 인스턴스화 된 정의 "Q.d"와 인스턴스화 된 보조 정리 "Q.l"을 생성 할 수 있습니다.
(4.) 이 새로운 이름 "Q.d"와 "Q.l"은 접두사 이름 "Q"로 시작됩니다.

Short ::
(1.) "Coq" is computer program to read and write mathematics .
(2.) A parameter "p" , which parametrizes many definitions "d" and lemmas "l" , may all be packaged into one .
(3.) Later on, this parameter "p" can be instantiated to create the instantiated definition "Q.d" and the instantiated secondary theorem "Q.l".
(4.) These new names "Q.d" and "Q.l" will be prefixed by any chosen prefix name "Q" .

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 . (**MEMO: 짧은 :: (1.) "Coq"는 수학 읽기와 쓰기를위한 컴퓨터 프로그램입니다 . (2.) 많은 정의 "d"와 보조 표제 "l"을 매개 변수화하는 매개 변수 "p"는 모두 하나에 패키지화 될 수 있습니다. (3.) 그런 다음 나중에이 매개 변수 "p"가 인스턴스화되어 인스턴스화 된 정의 "Q.d"와 인스턴스화 된 보조 정리 "Q.l"을 생성 할 수 있습니다. (4.) 이 새로운 이름 "Q.d"와 "Q.l"은 접두사 이름 "Q"로 시작됩니다. Short :: (1.) "Coq" is computer program to read and write mathematics . (2.) A parameter "p" , which parametrizes many definitions "d" and lemmas "l" , may all be packaged into one . (3.) Later on, this parameter "p" can be instantiated to create the instantiated definition "Q.d" and the instantiated secondary theorem "Q.l". (4.) These new names "Q.d" and "Q.l" will be prefixed by any chosen prefix name "Q" . Outline :: * PART 1 : SIMPLE PARAMETRIZATION * PART 2 : SIMPLE ENVIRONMENT * PART 3 : COMPLEX ENVIRONMENTAL PARAMETRIZATION *) (** PART 2 : SIMPLE ENVIRONMENT *) (** This does not lack to touch/call the Coq file [goptions.ml] ; it is hardcoded into the grammar *) 인쇄해 표 암시적인 입력들. (* Print Table Implicit Arguments . *) 설정해라 암시적인 입력들 . (* Set Implicit Arguments . *) 인쇄해 표 암시적인 입력들 . (* Print Table Implicit Arguments . *) 설정하지_말아라 암시적인 입력들. (* Unset Implicit Arguments *) 인쇄해 표 암시적인 입력들. (* Print Table Implicit Arguments . *) (*TODO *) Print Table Printing Let. 더해라 인쇄해 이라 prod. (* Add Printing Let prod. *) (*TODO *) Print Table Printing Let. 인쇄해 표 인쇄해 표기법 . (* Print Table Printing Notations. *) 설정해라 인쇄해 표기법 . (* Set Printing Notations. *) 인쇄해 표 인쇄해 표기법 . (* Print Table Printing Notations. *) 설정하지_말아라 인쇄해 표기법 . (* Unset Printing Notations. *)