Mysaa/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

README

Browse Source
This commit is contained in:
Adrien Vannson 2022-05-19 23:42:01 +02:00
parent 68887d6482
commit 81d53dc7a6
No known key found for this signature in database
GPG Key ID: FE2E66FD978C1A55
1 changed files with 10 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
README.md
View File

@ -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