coqtop - 클라우드의 온라인

프로그램:

이름

coqtop - Coq Proof Assistant 최상위 시스템

개요

콕탑 [ 옵션 ]

기술

콕탑 대화식 사용을 위한 Coq의 최상위 시스템입니다. 에 있는 문구를 읽습니다.
표준 입력, 표준 출력에 결과를 인쇄합니다.

Coq의 배치 지향 사용에 대해서는 다음을 참조하십시오. coqc(1).

옵션

-시간, --도움
돕다. coqtop에서 허용하는 전체 옵션 목록을 제공합니다.

-I 디렉토리, --포함하다 DIR
디렉토리 추가 DIR 포함 경로에서

-R DIR 콕디르
재귀적으로 물리적 매핑 DIR 논리적으로 콕디르

-상단 콕디르
최상위 이름을 다음으로 설정하십시오. 콕디르 탑 대신

-입력 상태 파일 이름, -는 파일 이름
파일에서 상태 읽기 파일명.coq

-소음 빈 초기 상태로 시작

-출력 상태파일 이름
파일에 상태 쓰기 파일명.coq

-load-ml-개체 파일 이름
ML 개체 파일 로드 파일명

-load-ml-소스 파일 이름
ML 파일 로드 파일 이름

-로드-버낙-소스 파일 이름, -l 파일 이름
Coq 파일 로드 파일명.v (파일 이름을 로드합니다.)

-로드-베르낙-소스-상세 파일 이름, -lv 파일 이름
세부적으로 Coq 파일 로드 파일명.v (자세한 파일 이름을 로드합니다.)

-로드 버낙 객체 파일 이름
Coq 개체 파일 로드 파일명.보

-필요하다 파일 이름
Coq 개체 파일 로드 파일명.보 가져오기(가져오기 파일 이름 필요)

-엮다 파일 이름
Coq 파일 컴파일 파일명.v (을(를) 암시 -일괄 )

-컴파일 장황 파일 이름
Coq 파일을 장황하게 컴파일 파일명.v (을(를) 암시 -일괄 )

-고르다 Coq의 네이티브 코드 버전 실행

-바이트 Coq의 바이트 코드 버전 실행

-어디 Coq의 표준 라이브러리 위치를 출력하고 종료합니다.

-v Coq 버전을 인쇄하고 종료

-q rcfile 로드 건너뛰기

-초기화 파일 파일 이름
rcfile을 다음으로 설정 파일 이름

-일괄 배치 모드(인수 구문 분석 직후 종료)

-신병 부팅 모드( -q 및 -일괄 )

-이맥스 Coq에게 Emacs에서 실행된다고 알려줍니다.

-덤프 글로브 파일 이름
파일 f의 덤프 세계화(에 의해 사용됨 coqdoc(1) )

- 지오프루프 포함 (예|아니요)
Coqide 내에서 Geoproof를 위한 특수 기능을 (비)활성화하기 위해(기본값은 예 )

- 암시적 집합
집합 정렬 암시적 집합

-내하중 방지
메모리에 불투명한 증명을 로드하지 마십시오

-xml XML 파일을 디렉토리에 뿌리를 둔 계층으로 내보냅니다.
$COQ_XML_LIBRARY_ROOT(설정된 경우) 또는 stdout(설정되지 않은 경우)

품질
일부 전술에 의해 생성된 증명 용어의 가독성 향상

onworks.net 서비스를 사용하여 coqtop 온라인 사용