Englishfrançaisespagnol

Icône de favori OnWorks

coq-tex - En ligne dans le Cloud

Exécutez coq-tex dans le fournisseur d'hébergement gratuit OnWorks sur Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS

Il s'agit de la commande coq-tex qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks en utilisant l'un de nos multiples postes de travail en ligne gratuits tels que Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS

PROGRAMME:

Nom


coq-tex - Traiter des phrases Coq intégrées dans des fichiers LaTeX

SYNOPSIS


coq tex [ -o fichier de sortie ] [ -n largeur de ligne ] [ -image image-coq ] [ -w ] [ -v ] [ -sl ] [
-hrule ] [ -petit ] fichier-entrée

DESCRIPTION


La coq tex le filtre extrait les phrases Coq intégrées dans les fichiers LaTeX, les évalue et
insérer le résultat de l'évaluation après chaque phrase.

Trois environnements LaTeX sont fournis pour inclure le code Coq dans les fichiers d'entrée :

coq_exemple
Les phrases entre \begin{coq_example} et \end{coq_example} sont évaluées et
copié dans le fichier de sortie. Chaque phrase est suivie de la réponse du
boucle de niveau supérieur.

coq_exemple*
Les phrases entre \begin{coq_example*} et \end{coq_example*} sont évaluées et
copié dans le fichier de sortie. Les réponses de la boucle de niveau supérieur sont rejetées.

coq_eval
Les phrases entre \begin{coq_eval} et \end{coq_eval} sont évaluées en silence.
Elles ne sont pas copiées dans le fichier de sortie, et les réponses de la boucle toplevel
sont mis au rebut.

Le code LaTeX résultant est stocké dans le fichier filet.v.tex si le fichier d'entrée porte le nom
la forme filet.tex, sinon le nom du fichier de sortie est le nom du fichier d'entrée
avec `.v.tex' ajouté.

Les fichiers produits par coq tex peut être directement traité par LaTeX. Les deux phrases Coq
et la sortie de niveau supérieur sont composées en police de machine à écrire.

OPTIONS


-o fichier de sortie
Spécifiez le nom d'un fichier où la sortie LaTeX doit être stockée. Un tiret "-"
provoque l'impression de la sortie LaTeX sur la sortie standard.

-n largeur de ligne
Définissez la largeur de ligne. La valeur par défaut est de 72 caractères. Les réponses du plus haut niveau
boucle sont pliés s'ils sont plus longs que la largeur de la ligne. Aucun pliage n'est effectué sur
le texte d'entrée Coq.

-image image-coq
Parce que le fichier image-coq à exécuter pour évaluer les phrases Coq. Par défaut,
c'est la commande coq sans spécifier de chemin utilisé pour évaluer
les phrases du Coq.

-w Faire en sorte que les lignes soient pliées sur un caractère espace dans la mesure du possible, en évitant les coupures de mots
dans la sortie. Par défaut, le pliage se produit à la largeur de la ligne, quel que soit le mot
coupes.

-v Mode verbeux. Imprime les réponses Coq sur la sortie standard. Utile pour détecter
erreurs dans les phrases Coq.

-sl Mode incliné. Les réponses Coq sont écrites dans une police inclinée.

-hrule Mode lignes horizontales. Les parties Coq sont écrites entre deux lignes horizontales.

-petit Mode petite police. Les parties Coq sont écrites dans une police plus petite.

MISES EN GARDE


Les phrases \begin... et \end... doivent se trouver sur une ligne par elles-mêmes, sans caractères
avant la barre oblique inverse ou après l'accolade fermante. Chaque phrase Coq doit se terminer par
`.' à la fin d'une ligne. Les espaces vides sont acceptés entre `.' et la nouvelle ligne, mais tout
un autre caractère fera que coq-tex ignore la fin de la phrase, ce qui entraîne un
mélange incorrect des réponses dans les phrases. (Les réponses « à la traîne ».)

Utilisez coq-tex en ligne en utilisant les services onworks.net


Serveurs et postes de travail gratuits

Télécharger des applications Windows et Linux

  • 1
    Responsable PAC
    Responsable PAC
    PAC est un remplacement de Perl/GTK pour
    SecureCRT/Putty/etc (linux
    ssh/telnet/... gui)... Il fournit une interface graphique
    configurer les connexions : utilisateurs,
    mots de passe, règle EXPECT...
    Télécharger PAC Manager
  • 2
    GeoServer
    GeoServer
    GeoServer est un logiciel open source
    serveur écrit en Java qui permet aux utilisateurs
    pour partager et éditer des données géospatiales.
    Conçu pour l'interopérabilité, il
    publie da...
    Télécharger GeoServer
  • 3
    Luciole III
    Luciole III
    Une finance personnelle gratuite et open-source
    gestionnaire. Firefly III dispose d'un
    système de comptabilité en partie double. Vous pouvez
    entrez et organisez rapidement votre
    opérations je...
    Télécharger Firefly III
  • 4
    Extensions Apache OpenOffice
    Extensions Apache OpenOffice
    Le catalogue officiel d'Apache
    Extensions OpenOffice. Tu trouveras
    des extensions allant des dictionnaires aux
    outils pour importer des fichiers PDF et se connecter
    avec ext...
    Télécharger les extensions Apache OpenOffice
  • 5
    MantisBT
    MantisBT
    Mantis est un outil Web facilement déployable
    bugtracker basé pour aider le bogue du produit
    suivi. Il nécessite PHP, MySQL et un
    serveur Web. Découvrez notre démo et hébergé
    offre...
    Télécharger MantisBT
  • 6
    LAN Messenger
    LAN Messenger
    LAN Messenger est une application de chat p2p
    pour la communication intranet et ne
    besoin d'un serveur. Une variété de pratiques
    les fonctionnalités sont prises en charge, y compris
    aviser...
    Télécharger LAN Messenger
  • Plus "

Commandes Linux

  • 1
    abidw
    abidw
    abidw - sérialiser l'ABI d'un ELF
    fichier abidw lit une bibliothèque partagée dans ELF
    formate et émet une représentation XML
    de son ABI à la sortie standard. Le
    émis...
    Courez abidw
  • 2
    capable
    capable
    abilint - valider un Abigail ABI
    la représentation abilint analyse le natif
    Représentation XML d'un ABI tel qu'émis
    par abidw. Une fois qu'il a analysé le XML
    représenter...
    Exécuter Abilint
  • 3
    coresendmsg
    coresendmsg
    coresendmsg - envoyer un message API CORE
    au démon core-daemon...
    Exécutez coresendmsg
  • 4
    serveur_noyau
    serveur_noyau
    core_server - Le serveur principal pour
    Spam Bayes. DESCRIPTION : Sert actuellement
    l'interface Web uniquement. Branchement
    auditeurs pour divers protocoles est à définir.
    Cette ...
    Exécutez core_server
  • 5
    flash fw
    flash fw
    fwflash - programme pour flasher le fichier image
    à un appareil NXT connecté ...
    Exécutez fwflash
  • 6
    fwts-collecte
    fwts-collecte
    fwts-collect - collecte les journaux pour fwts
    rapport de bogue. ...
    Exécutez fwts-collect
  • Plus "

Ad