Este es el comando coq-tex que se puede ejecutar en el proveedor de alojamiento gratuito de OnWorks utilizando una de nuestras múltiples estaciones de trabajo en línea gratuitas, como Ubuntu Online, Fedora Online, emulador en línea de Windows o emulador en línea de MAC OS.
PROGRAMA:
NOMBRE
coq-tex - Procesar frases de Coq incrustadas en archivos LaTeX
SINOPSIS
coq-tex [ -o archivo de salida ] [ -n ancho de línea ] [ -imagen coq-imagen ] [ -w ] [ -v ] [ -sl ] [
-hrule ] [ -pequeña ] fichero de entrada ...
DESCRIPCIÓN
La coq-tex filter extrae frases Coq incrustadas en archivos LaTeX, las evalúa y
inserte el resultado de la evaluación después de cada frase.
Se proporcionan tres entornos LaTeX para incluir código Coq en los archivos de entrada:
ejemplo_coq
Las frases entre \ begin {coq_example} y \ end {coq_example} se evalúan y
copiado en el archivo de salida. Cada frase va seguida de la respuesta del
bucle de nivel superior.
coq_example *
Las frases entre \ begin {coq_example *} y \ end {coq_example *} se evalúan y
copiado en el archivo de salida. Las respuestas del bucle de nivel superior se descartan.
coq_eval
Las frases entre \ begin {coq_eval} y \ end {coq_eval} se evalúan en silencio.
No se copian en el archivo de salida y las respuestas del bucle de nivel superior
se descartan.
El código LaTeX resultante se almacena en el archivo presentar.v.tex si el archivo de entrada tiene el nombre
la forma presentar.tex, de lo contrario, el nombre del archivo de salida es el nombre del archivo de entrada
con '.v.tex' adjunto.
Los archivos producidos por coq-tex puede ser procesado directamente por LaTeX. Ambas frases de Coq
y la salida de nivel superior están compuestas en fuente de máquina de escribir.
OPCIONES
-o archivo de salida
Especifique el nombre de un archivo donde se almacenará la salida LaTeX. Un guión '-'
hace que la salida LaTeX se imprima en la salida estándar.
-n ancho de línea
Establece el ancho de la línea. El valor predeterminado es 72 caracteres. Las respuestas del nivel superior
Los bucles se doblan si son más largos que el ancho de la línea. No se realiza ningún plegado en
el texto de entrada de Coq.
-imagen coq-imagen
Porque el archivo coq-imagen a ejecutar para evaluar las frases Coq. Por defecto,
este es el comando coqueta sin especificar ninguna ruta que se utilice para evaluar
las frases de Coq.
-w Hacer que las líneas se doblen en un carácter de espacio siempre que sea posible, evitando cortes de palabras
en la salida. De forma predeterminada, el plegado se produce en el ancho de línea, independientemente de la palabra
cortes.
-v Modo detallado. Imprime las respuestas de Coq en la salida estándar. Útil para detectar
errores en frases Coq.
-sl Modo inclinado. Las respuestas de Coq están escritas en una fuente inclinada.
-hrule Modo de líneas horizontales. Las partes de Coq están escritas entre dos líneas horizontales.
-pequeña Modo de fuente pequeña. Las partes de Coq están escritas en una fuente más pequeña.
AVISOS
Las frases \ begin ... y \ end ... deben ubicarse en una línea por sí mismas, sin caracteres
antes de la barra invertida o después de la llave de cierre. Cada frase de Coq debe terminar con
'.' al final de una línea. Se aceptan espacios en blanco entre '.' y la nueva línea, pero cualquier
otro carácter hará que coq-tex ignore el final de la frase, dando como resultado un
Mezcla incorrecta de las respuestas en las frases. (Las respuestas `` se quedan atrás ''.)
Use coq-tex en línea usando los servicios de onworks.net
