Este es el comando coqtop 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
coqtop - El sistema de nivel superior Coq Proof Assistant
SINOPSIS
coqueta [ opciones ]
DESCRIPCIÓN
coqueta es el sistema de nivel superior de Coq, para uso interactivo. Lee frases en el
entrada estándar e imprime los resultados en la salida estándar.
Para el uso de Coq orientado a lotes, consulte coqc(1).
OPCIONES
-h, --ayuda
Ayudar. Le dará la lista completa de opciones aceptadas por coqtop.
-I es, --incluir dir
agregar directorio dir en la ruta de inclusión
-R dir coqdir
mapear recursivamente físico dir a la lógica coqdir
-parte superior coqdir
establecer el nombre de nivel superior en coqdir en lugar de Top
-estado de entrada nombre del archivo, -es nombre de archivo
leer el estado del archivo nombredearchivo.coq
-ruido empezar con un estado inicial vacío
estado de salidanombre de archivo
escribir estado en archivo nombredearchivo.coq
-carga-ml-objeto nombre de archivo
cargar archivo de objeto ML nombre de archivo
-carga-ml-fuente nombre de archivo
cargar archivo ML nombre de archivo
-cargar-fuente-vernac nombre del archivo, -l nombre de archivo
cargar archivo Coq nombrearchivo.v (Cargar nombre de archivo).
-load-vernac-fuente-detallada nombre del archivo, -lv nombre de archivo
cargar el archivo Coq verbosely nombrearchivo.v (Cargar nombre de archivo detallado).
-cargar-objeto-vernac nombre de archivo
cargar archivo de objeto Coq nombrearchivo.vo
-exigir nombre de archivo
cargar archivo de objeto Coq nombrearchivo.vo e importarlo (Requerir nombre de archivo de importación).
-compilar nombre de archivo
compilar archivo Coq nombrearchivo.v (implica -lote )
-compilar-detallado nombre de archivo
compilar detalladamente el archivo Coq nombrearchivo.v (implica -lote )
-optar ejecutar la versión de código nativo de Coq
-byte ejecutar la versión de código de bytes de Coq
-dónde imprimir la ubicación de la biblioteca estándar de Coq y salir
-v imprimir la versión de Coq y salir
-q omitir la carga de rcfile
-archivo-inicial nombre de archivo
establecer el rcfile en nombre de archivo
-lote modo por lotes (sale justo después del análisis de argumentos)
-bota modo de arranque (implica -q y -lote )
-emacs le dice a Coq que se ejecuta bajo Emacs
-volcado-glob nombre de archivo
volcar globalizaciones en el archivo f (para ser utilizado por coqdoc(1) )
-con-geoproof (si | no)
para (des) activar funciones especiales para Geoproof dentro de Coqide (por defecto es si )
-conjunto-impredicativo
establecer ordenación Establecer impredicativo
-no-pruebas-de-carga
no cargue pruebas opacas en la memoria
-xml exportar archivos XML a la jerarquía enraizada en el directorio
$ COQ_XML_LIBRARY_ROOT (si está configurado) o stdout (si no está configurado)
Calidad
mejorar la legibilidad de los términos de prueba producidos por algunas tácticas
Use coqtop en línea usando los servicios de onworks.net
