InglésFrancésCursos de

icono de página de OnWorks

coqide.byte - Online en la nube

Ejecute coqide.byte en el proveedor de alojamiento gratuito de OnWorks sobre Ubuntu Online, Fedora Online, emulador en línea de Windows o emulador en línea de MAC OS

Este es el comando coqide.byte 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


coqide - La interfaz gráfica Coq Proof Assistant

SINOPSIS


coquide [ opciones ]

DESCRIPCIÓN


coquide es una interfaz gráfica gtk para el asistente de pruebas Coq.

Para el uso de Coq orientado a la línea de comandos, consulte coqueta(1); para el uso de Coq orientado a lotes, consulte
coqc(1).

OPCIONES


-h Mostrar la lista completa de opciones aceptadas por coquide.

-I dir, -incluir dir
Agregue directorio de directorio en la ruta de inclusión.

-R dir coqdir
Mapeo físico recursivo dir a la lógica coqdir.

-origen Agregue directorios de origen en la ruta de inclusión.

-es f, -estado de entrada f
Leer estado de f.coq.

-ruido Comience con un estado vacío.

estado de salida f
Escribir estado en archivo f.coq.

-carga-ml-objeto f
Cargar archivo de objeto ML f.

-carga-ml-fuente f
Cargar archivo ML f.

-l f, -cargar-fuente-vernac f
Cargar archivo Coq f.v (Cargar f.).

-lv f, -load-vernac-fuente-detallada f
Cargar archivo Coq f.v (carga detallada f.).

-cargar-objeto-vernac f
Cargar archivo de objeto Coq f.vo.

-exigir f
Cargar archivo de objeto Coq f.vo e importarlo (Requerir f.).

-compilar f
Compilar archivo Coq f.v (implica -lote).

-compilar-detallado f
Compilar detalladamente el archivo Coq f.v (implica -lote).

-optar Ejecute la versión de código nativo de Coq o Coq_SearchIsos.

-byte Ejecute la versión de código de bytes de Coq o Coq_SearchIsos.

-dónde Imprima la ubicación de la biblioteca estándar de Coq y salga.

-v Imprime la versión de Coq y sal.

-q Omitir la carga de rcfile.

-archivo-inicial f
Establezca el rcfile en f.

-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 en Emacs.

-volcado-glob f
Volcar globalizaciones en archivo f (ser usado por coqdoc(1)).

-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).

Use coqide.byte en línea usando los servicios de onworks.net


Servidores y estaciones de trabajo gratuitos

Descargar aplicaciones de Windows y Linux

  • 1
    huelga
    huelga
    Proyecto Strikr Free Software. Artefactos
    publicado bajo un 'basado en la intención'
    licencia dual: AGPLv3 (comunidad) y
    CC-BY-NC-ND 4.0 internacional
    (comercial)...
    descargar strikr
  • 3
    GIFLIB
    GIFLIB
    giflib es una biblioteca para leer y
    escribiendo imágenes gif. Es API y ABI
    compatible con libungif que estaba en
    amplio uso mientras que la compresión LZW
    el algoritmo fue...
    Descargar GIFLIB
  • 4
    Alt-F
    Alt-F
    Alt-F proporciona un código abierto y gratuito
    firmware alternativo para DLINK
    DNS-320/320L/321/323/325/327L and
    DNR-322L. Alt-F tiene Samba y NFS;
    soporta ext2 / 3/4 ...
    Descargar Alt-F
  • 5
    usm
    usm
    Usm es un paquete de slackware unificado
    gerente que maneja automático
    resolución de dependencia. unifica
    varios repositorios de paquetes, incluidos
    slackware, flojo, p...
    Descargar usm
  • 6
    Chart.js
    Chart.js
    Chart.js es una biblioteca Javascript que
    permite a los diseñadores y desarrolladores dibujar
    todo tipo de gráficos usando HTML5
    elemento de lienzo Chart js ofrece una gran
    matriz ...
    Descargar Chart.js
  • Más "

Comandos de Linux

Ad