This commit is contained in:
Adrien Vannson 2022-05-18 11:20:39 +02:00
parent bbfdad1b78
commit aa0b71bfc9
No known key found for this signature in database
GPG Key ID: FE2E66FD978C1A55

View File

@ -1,9 +1,9 @@
The Pieuvre™ Proof Assistant 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, que vos cerveaux primitifs biaisés vous pousseraient à croire. C'est que vous avez besoin du réconfort de pieuvre !
Pieuvre™ est un assitant de preuve à votre service. Lorsque vous doutez, êtes éffrayé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, ê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é. 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é.
@ -40,8 +40,10 @@ L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s'
### Adrien ### Adrien
- Option `typecheck` - Option `typecheck`
- Partie interactive
### Samy ### Samy
Introduction du README
Fonctions de manipulation des λ-termes (pieuvre.ml) Fonctions de manipulation des λ-termes (pieuvre.ml)
Typecheck Typecheck
Erreurs lors des tactiques. Erreurs lors des tactiques.