Đây là lệnh coq-tex có thể chạy trong nhà cung cấp dịch vụ lưu trữ miễn phí OnWorks bằng cách sử dụng một trong nhiều máy trạm trực tuyến miễn phí của chúng tôi như Ubuntu Online, Fedora Online, trình giả lập trực tuyến Windows hoặc trình giả lập trực tuyến MAC OS
CHƯƠNG TRÌNH:
TÊN
coq-tex - Xử lý các cụm từ Coq được nhúng trong tệp LaTeX
SYNOPSIS
coq-tex [ -o tập tin đầu ra ] [ -n chiều rộng dòng ] [ -hình ảnh hình ảnh coq ] [ -w ] [ -v ] [ -sl ] [
-hrule ] [ -nhỏ ] tập tin đầu vào ...
MÔ TẢ
Sản phẩm coq-tex bộ lọc trích xuất các cụm từ Coq được nhúng trong tệp LaTeX, đánh giá chúng và
chèn kết quả đánh giá sau mỗi cụm từ.
Ba môi trường LaTeX được cung cấp để bao gồm mã Coq trong các tệp đầu vào:
coq_example
Các cụm từ giữa \ begin {coq_example} và \ end {coq_example} được đánh giá và
được sao chép vào tệp đầu ra. Theo sau mỗi cụm từ là phản hồi của
vòng lặp cấp trên.
coq_example *
Các cụm từ giữa \ begin {coq_example *} và \ end {coq_example *} được đánh giá và
được sao chép vào tệp đầu ra. Các phản hồi của vòng lặp cấp cao nhất bị loại bỏ.
coq_eval
Các cụm từ giữa \ begin {coq_eval} và \ end {coq_eval} được đánh giá âm thầm.
Chúng không được sao chép vào tệp đầu ra và các phản hồi của vòng lặp cấp trên
bị loại bỏ.
Mã LaTeX kết quả được lưu trữ trong tệp hồ sơ.v.tex nếu tệp đầu vào có tên là
hình thức hồ sơ.tex, nếu không thì tên của tệp đầu ra là tên của tệp đầu vào
với '.v.tex' được thêm vào.
Các tệp được tạo ra bởi coq-tex có thể được xử lý trực tiếp bởi LaTeX. Cả hai cụm từ Coq
và đầu ra ở mức cao nhất được sắp chữ trong phông chữ của máy đánh chữ.
LỰA CHỌN
-o tập tin đầu ra
Chỉ định tên của tệp nơi đầu ra LaTeX sẽ được lưu trữ. Dấu gạch ngang `- '
khiến đầu ra LaTeX được in trên đầu ra tiêu chuẩn.
-n chiều rộng dòng
Đặt chiều rộng dòng. Giá trị mặc định là 72 ký tự. Các phản hồi của toplevel
vòng lặp được gấp lại nếu chúng dài hơn chiều rộng dòng. Không có thao tác gấp nào được thực hiện trên
văn bản đầu vào Coq.
-hình ảnh hình ảnh coq
Gây ra tệp hình ảnh coq được thực thi để đánh giá các cụm từ Coq. Theo mặc định,
đây là lệnh coqtop mà không chỉ định bất kỳ đường dẫn nào được sử dụng để đánh giá
các cụm từ Coq.
-w Làm cho các dòng được gấp trên một ký tự khoảng trắng bất cứ khi nào có thể, tránh bị cắt từ
trong đầu ra. Theo mặc định, gấp xảy ra ở độ rộng dòng, bất kể từ nào
các vết cắt.
-v Chế độ chi tiết. In câu trả lời Coq trên đầu ra tiêu chuẩn. Hữu ích để phát hiện
lỗi trong cụm từ Coq.
-sl Chế độ nghiêng. Các câu trả lời Coq được viết bằng phông chữ nghiêng.
-hrule Chế độ đường ngang. Phần Coq được viết giữa hai dòng ngang.
-nhỏ Chế độ phông chữ nhỏ. Các phần Coq được viết bằng phông chữ nhỏ hơn.
THẬN TRỌNG
Các cụm từ \ begin ... và \ end ... phải tự nằm trên một dòng, không có ký tự
trước dấu gạch chéo ngược hoặc sau dấu ngoặc nhọn. Mỗi cụm từ Coq phải được kết thúc bằng
`. ' ở cuối dòng. Khoảng trống được chấp nhận giữa '.' và dòng mới, nhưng bất kỳ
ký tự khác sẽ khiến coq-tex bỏ qua phần cuối của cụm từ, dẫn đến
xáo trộn các câu trả lời thành các cụm từ không chính xác. (Các câu trả lời `` tụt hậu ''.)
Sử dụng coq-tex trực tuyến bằng các dịch vụ onworks.net
