diff --git a/README.md b/README.md index c07fc00..61dd5b1 100644 --- a/README.md +++ b/README.md @@ -1,9 +1,9 @@ The Pieuvre™ Proof Assistant ============================ -Ne vous êtes jamais vous dit que votre quotidien était morose ? Que tout ce que vous pourriez prouver dans votre vie ne serait que vain, que vos cerveaux primitifs biaisés vous pousseraient à croire. C'est que vous avez besoin du réconfort de pieuvre ! +Ne vous êtes jamais vous dit que votre quotidien était morose ? Que tout ce que vous pourriez prouver dans votre vie ne serait que vain ? C'est que vous avez besoin du réconfort de Pieuvre™ ! -Pieuvre™ est un assistant de preuve à votre service. Lorsque vous doutez, êtes effrayés par l'incurable finitude de votre esprit, l'ineffable efficacité de Pieuvre™ saura vous réconforter en vous assurant des preuves complètes et sans accroc. +Pieuvre™ est un assistant de preuve à votre service. Lorsque vous doutez, que vous êtes effrayés par l'incurable finitude de votre esprit, l'ineffable efficacité de Pieuvre™ saura vous réconforter en vous assurant des preuves complètes et sans accroc. Bien plus efficace que d'autres gallinacés, l'interface CLI de Pieuvre™ saura convenir à petits et grands. Son design entre post-modernisme et romantisme baroque néo-mérovingien rappellera aux utilisateur·ices les plus avertis les plus grandes heures de l'humanité. @@ -12,10 +12,10 @@ Allez, tous à vos pieuvres ! *L'équipe de Pieuvre™ n'est pas responsable des dommages occasionnés par les réalisations philosophiques causées aux utilisateur·ices de par l'utilisation du programme* # Utilisation -`Pieuvre` génère automatiquement un fichier `log.8pus` contenant la preuve venant d'être faite. Attention, le fichier `log.8pus` ne doit jamais être donné en entrée de pieuvre ! +`Pieuvre` génère automatiquement un fichier `log.8pus` contenant la preuve venant d'être faite. Attention, le fichier `log.8pus` ne doit jamais être donné en entrée de Pieuvre™ ! ## Option `typecheck` -L'option `typecheck` peut être testée avec les fichiers tests dans `tests/typecheck`. Pour cela, utiliser les commandes : +L'option `typecheck` vérifie si un lambda-terme est bien typé. Elle s'utilise de la manière suivante : ``` ./pieuvre -typecheck tests/typecheck/right-type ./pieuvre -typecheck tests/typecheck/wrong-type @@ -37,8 +37,11 @@ L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s' ## Répartition du travail ### Adrien -- Option `typecheck` -- Partie interactive +- Interface interactive (avec le parsage des formules, des tactiques, ...), lecture des fichiers +- Construction d'un lambda-terme à partir de la preuve (sans et / ou ) +- Tactiques élémentaires (`intro`, `intros`, `assumption`, `apply`, `elim`) +- Options `alpha`, `reduce`, `typecheck`, ... : partie interactive appelant les fonctions écrites par Samy +- Écriture de tests (irréfutabilité du tiers exclus, de la formule de Peirce, ...) ### Samy - Introduction du README @@ -49,3 +52,4 @@ L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s' - Parsing des λ-termes - `True` et `exact` - Option `-computetype` +- Écriture de tests