Dit is de opdracht coqmktop die kan worden uitgevoerd in de gratis hostingprovider van OnWorks met behulp van een van onze meerdere gratis online werkstations zoals Ubuntu Online, Fedora Online, Windows online emulator of MAC OS online emulator
PROGRAMMA:
NAAM
coqmktop - De Coq Proof Assistant-gebruiker-tactiek-linker
KORTE INHOUD
koktop [ opties ] bestanden
PRODUCTBESCHRIJVING
koktop bouwt een nieuw Coq-topniveau uitgebreid met gebruikerstactieken. bestanden zijn de doelstelling
Caml-object- of bibliotheekbestanden (dwz met het achtervoegsel .cmo, .cmx, .cma of .cmxa) om te koppelen met de
Coq-systeem. De linker produceert een uitvoerbaar Coq-topniveau dat direct kan worden aangeroepen
of doorheen coqc(1), met behulp van de optie -image.
OPTIES
-h Hulp. Maak een lijst van de beschikbare opties.
-srcdir dir
Geef op waar de Coq-bronbestanden zich bevinden
-o exec-bestand
Geef de naam op van het resulterende topniveau
-opt Compileer in native code
-full Koppel tactieken op hoog niveau
-bovenkant Bouw Coq op een ocaml-topniveau (niet compatibel met -opt)
-R dir Geef recursief mappen op voor Ocaml
-v8 Koppeling met V8-grammatica
Gebruik coqmktop online met behulp van onworks.net-services
