Este es el comando hol-light 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
hol-light - demostrador interactivo de teoremas de HOL Light
SINOPSIS
hol-luz [opciones ...]
DESCRIPCIÓN
El comando hol-luz es un contenedor simple para llamar ocaml y cargando la luz HOL
definiciones básicas (cargando /usr/share/hol-luz/hol.ml en lugar de .ocamlinit as
archivo de inicialización). La carga de estas definiciones lleva aproximadamente 2 minutos en hardware moderno,
por favor sea paciente. Todas las opciones y otros argumentos se pasan como opciones a ocaml.
Si usted tiene una editor de línea de lectura como envoltura, dijo or vida instalado, el hol-luz ocaml
toplevel está envuelto en editor de línea de lectura. Instale solo uno de estos editores readline o
configure su preferido a través del sistema alternativo.
Use hol-light en línea usando los servicios de onworks.net
