Ubuntu Online, Fedora Online, Windows 온라인 에뮬레이터 또는 MAC OS 온라인 에뮬레이터와 같은 여러 무료 온라인 워크스테이션 중 하나를 사용하여 OnWorks 무료 호스팅 공급자에서 실행할 수 있는 coq-tex 명령입니다.
프로그램:
이름
coq-tex - LaTeX 파일에 포함된 Coq 문구 처리
개요
콕텍스 [ -o 결과물 파일 ] [ -n 선의 폭 ] [ -영상 coq 이미지 ] [ -w ] [ -v ] [ -sl ] [
-hrule ] [ -작은 ] 입력 파일 ...
기술
이 어플리케이션에는 XNUMXµm 및 XNUMXµm 파장에서 최대 XNUMXW의 평균 출력을 제공하는 콕텍스 필터는 LaTeX 파일에 포함된 Coq 구문을 추출하고 이를 평가하며
각 구 뒤에 평가 결과를 삽입합니다.
입력 파일에 Coq 코드를 포함하기 위해 세 가지 LaTeX 환경이 제공됩니다.
coq_예제
\begin{coq_example}과 \end{coq_example} 사이의 구문이 평가되고
출력 파일에 복사됩니다. 각 문구 뒤에는 응답자의 응답이 이어집니다.
최상위 루프.
coq_예*
\begin{coq_example*}과 \end{coq_example*} 사이의 구문이 평가되고
출력 파일에 복사됩니다. 최상위 루프의 응답은 무시됩니다.
coq_eval
\begin{coq_eval}과 \end{coq_eval} 사이의 구문은 자동으로 평가됩니다.
출력 파일에 복사되지 않으며 최상위 루프의 응답
폐기됩니다.
결과 LaTeX 코드는 파일에 저장됩니다. 파일.v.tex 입력 파일의 이름이
형태 파일.tex, 그렇지 않으면 출력 파일의 이름은 입력 파일의 이름입니다.
`.v.tex'가 추가되었습니다.
에 의해 생성된 파일 콕텍스 LaTeX에서 직접 처리할 수 있습니다. Coq 문구 모두
최상위 출력은 타자기 글꼴로 조판됩니다.
옵션
-o 결과물 파일
LaTeX 출력이 저장될 파일의 이름을 지정하십시오. 대시 `-'
LaTeX 출력이 표준 출력으로 인쇄되도록 합니다.
-n 선의 폭
선 너비를 설정합니다. 기본값은 72자입니다. 최상위 레벨의 응답
루프가 선 너비보다 길면 루프가 접힙니다. 접기가 수행되지 않습니다.
Coq 입력 텍스트.
-영상 coq 이미지
원인 파일 coq 이미지 Coq 문구를 평가하기 위해 실행됩니다. 기본적으로,
이것은 명령이다 콕탑 평가에 사용되는 경로를 지정하지 않고
Coq 문구.
-w 단어 잘림을 피하면서 가능할 때마다 줄을 공백 문자로 접습니다.
출력에서. 기본적으로 접기는 단어에 관계없이 선 너비에서 발생합니다.
컷.
-v 상세 모드. 표준 출력에 Coq 답변을 인쇄합니다. 탐지에 유용
Coq 문구의 오류.
-sl 기울어진 모드. Coq 답변은 기울어진 글꼴로 작성됩니다.
-hrule 수평선 모드. Coq 부분은 두 개의 수평선 사이에 작성됩니다.
-작은 작은 글꼴 모드. Coq 부분은 더 작은 글꼴로 작성됩니다.
경고
\begin... 및 \end... 구는 문자 없이 한 줄에 있어야 합니다.
백슬래시 앞 또는 닫는 중괄호 뒤. 각 Coq 문구는 다음으로 끝나야 합니다.
`.' 줄 끝에. `.' 사이에 공백이 허용됩니다. 줄 바꿈이지만
다른 문자는 coq-tex가 구문의 끝을 무시하게 하여
응답을 구문으로 잘못 섞습니다. (응답이 ``지연''합니다.)
onworks.net 서비스를 사용하여 온라인에서 coq-tex 사용
