EngelsFransSpaans

OnWorks-favicon

coqtop - Online in de cloud

Voer coqtop uit in de gratis hostingprovider van OnWorks via Ubuntu Online, Fedora Online, Windows online emulator of MAC OS online emulator

Dit is de opdracht coqtop 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


coqtop - Het Coq Proof Assistant toplevelsysteem

KORTE INHOUD


koktop [ opties ]

PRODUCTBESCHRIJVING


koktop is het toplevelsysteem van Coq, voor interactief gebruik. Het leest zinnen op de
standaardinvoer en drukt de resultaten af ​​op de standaarduitvoer.

Voor batchgericht gebruik van Coq, zie coqc(1).

OPTIES


-H, --help
Hulp. Geeft u de volledige lijst met opties die door coqtop worden geaccepteerd.

-I richt, --erbij betrekken dir
map toevoegen dir in het include-pad

-R dir coqdir
recursief fysiek in kaart brengen dir logisch coqdir

-bovenkant coqdir
stel de naam op het hoogste niveau in coqdir in plaats van Top

-invoerstatus bestandsnaam, -is bestandsnaam
status uit bestand lezen bestandsnaam.coq

-Nee is beginnen met een lege begintoestand

-uitvoerstatusbestandsnaam
schrijf status in bestand bestandsnaam.coq

-load-ml-object bestandsnaam
ML-objectbestand laden bestandsnaam

-load-ml-bron bestandsnaam
ML-bestand laden bestandsnaam

-laad-vernac-bron bestandsnaam, -l bestandsnaam
Coq-bestand laden bestandsnaam.v (Laad bestandsnaam.)

-load-vernac-source-uitgebreid bestandsnaam, -lv bestandsnaam
laad het Coq-bestand uitgebreid bestandsnaam.v (Laad uitgebreide bestandsnaam.)

-load-vernac-object bestandsnaam
laad het Coq-objectbestand bestandsnaam.vo

-vereisen bestandsnaam
laad het Coq-objectbestand bestandsnaam.vo en importeer het (vereist importbestandsnaam.)

-compileren bestandsnaam
Coq-bestand compileren bestandsnaam.v (impliceert -partij )

-compileer-uitgebreid bestandsnaam
compileer Coq-bestand uitvoerig bestandsnaam.v (impliceert -partij )

-opt voer de native-codeversie van Coq uit

-byte voer de bytecodeversie van Coq uit

-waar druk de standaardbibliotheeklocatie van Coq af en sluit af

-v druk de Coq-versie af en sluit af

-q sla het laden van rcfile over

-init-bestand bestandsnaam
stel het rcbestand in op bestandsnaam

-partij batchmodus (wordt afgesloten net na het parseren van de argumenten)

-laars opstartmodus (impliceert -q en -partij )

-emacs vertelt Coq dat het wordt uitgevoerd onder Emacs

-dump-glob bestandsnaam
dump globalisaties in bestand f (te gebruiken door coqdoc(1) )

-met-geoproof (ja|nee)
om speciale functies voor Geoproof binnen Coqide te (de)activeren (standaard is ja )

-impredicatieve-set
set sort Stel impredicatief in

-dont-load-bewijzen
laad geen ondoorzichtige proefdrukken in het geheugen

-xml exporteer XML-bestanden naar de hiërarchie die in de map is geworteld
$COQ_XML_LIBRARY_ROOT (indien ingesteld) of naar stdout (indien niet ingesteld)

-Kwaliteit
de leesbaarheid verbeteren van de bewijstermen die door sommige tactieken worden geproduceerd

Gebruik coqtop online met behulp van onworks.net-services


Gratis servers en werkstations

Windows- en Linux-apps downloaden

  • 1
    MSYS2
    MSYS2
    MSYS2 is een verzameling tools en
    bibliotheken die u voorzien van een
    gebruiksvriendelijke omgeving om te bouwen,
    native Windows installeren en uitvoeren
    software. Het gaat om...
    MSYS2 downloaden
  • 2
    libjpeg-turbo
    libjpeg-turbo
    libjpeg-turbo is een JPEG-afbeeldingscodec
    die SIMD-instructies gebruikt (MMX, SSE2,
    NEON, AltiVec) om de basislijn te versnellen
    JPEG-compressie en -decompressie aan
    x86, x8...
    Libjpeg-turbo downloaden
  • 3
    Xtreme Download Manager
    Xtreme Download Manager
    Het project heeft nu een nieuwe thuis:
    https://xtremedownloadmanager.com/ For
    ontwikkelaars:
    https://github.com/subhra74/xdm Xtreme
    Download Manager is een krachtige tool om...
    Xtreme-downloadmanager downloaden
  • 4
    TTGO VGA32 Lite
    TTGO VGA32 Lite
    Kenmerken:4:3 en 16:9 lage resolutie
    VGA-uitgangPS/2 toetsenbord en muis
    inputText-gebaseerde gebruikersinterface (TUI)
    met dialoogmanagerGedeeltelijke Unicode
    ondersteuningSlave dis...
    TTGO VGA32 Lite downloaden
  • 5
    Clover EFI-bootloader
    Clover EFI-bootloader
    Project is verplaatst naar
    https://github.com/CloverHackyColor/CloverBootloader..
    Functies:Boot macOS, Windows en Linux
    in UEFI of legacy-modus op Mac of pc met
    EU...
    Download Clover EFI-bootloader
  • 6
    verenigde rpms
    verenigde rpms
    Doe mee met Gitter!
    https://gitter.im/unitedrpms-people/Lobby
    Schakel de URPMS-repository in uw
    systeem -
    https://github.com/UnitedRPMs/unitedrpms.github.io/bl...
    Unitedrpms downloaden
  • Meer "

Linux-commando's

Ad