짧은 :: "Coq"는 수학 읽기와 쓰기를위한 컴퓨터 프로그램입니다 .
"Coq"는 복잡한 계산을 수행 할 수 있습니다.
"Coq"는 간단한 계산을 수행 할 수도 있습니다.
예 : "Coq"는 요소들 [ "참된, 그릇된"]만을 포함하는 간단한 데이터에 대한 계산을 수행 할 수 있습니다. 이러한 간단한 계산은 "논리"라고합니다.

Short :: "Coq" is computer program to read and write mathematics .
"Coq" can do complex calculations .
"Coq" can also do simple calculations .
Example : "Coq" can do computations on the simple data which contains only the elements [ "true , false" ] . These simple computations are named "logic" .

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"애드온을 활성화하십시오 : 표준 라이브러리의 정책 및 보조 정리 이름을 자동으로 완성하고 오른쪽 창에 부트 유형을 표시하십시오.