Il s'agit de la commande gallina 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
gallina - extrait les spécifications des fichiers vernaculaires Coq
SYNOPSIS
poule [ - ] [ -sortie standard ] [ -Sans commentaires ] filet ...
DESCRIPTION
poule prend les fichiers Coq comme arguments et construit les fichiers de spécifications correspondants.
Le fichier Coq foo.v donne du poids au dossier de spécification foo.g. Le suffixe '.g' signifie
pour Gallina.
Pour cela, gallina supprime toutes les commandes qui suivent un "Théorème", "Lemme", "Fait",
Instruction "Remark" ou "Objectif" jusqu'à ce qu'elle atteigne une commande "Abort.", "Save.", "Qed.",
"Défini." ou "Preuve <...>.". Il supprime également chaque "Indice", "Syntaxe", "Immédiat" ou
Commande "Transparente".
Les fichiers sans le suffixe .v sont ignorés.
OPTIONS
-sortie standard
Imprime le résultat sur la sortie standard.
- La source Coq est prise sur l'entrée standard. Le résultat est imprimé sur la sortie standard.
-Sans commentaires
Les commentaires sont supprimés dans le fichier *.g.
NOTES
Les commentaires imbriqués sont correctement traités. En particulier, chaque commande "Enregistrer". ou "Abandonner". dans
un commentaire n'est pas pris en compte.
Utilisez gallina en ligne en utilisant les services onworks.net
