From aa0b71bfc9ebe5ab98dd6fab151f5cedeced3fb8 Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Wed, 18 May 2022 11:20:39 +0200 Subject: [PATCH] README --- README.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index d6f9798..fcb4b2b 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 ! -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é. @@ -40,8 +40,10 @@ L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s' ### Adrien - Option `typecheck` +- Partie interactive ### Samy +Introduction du README Fonctions de manipulation des λ-termes (pieuvre.ml) Typecheck Erreurs lors des tactiques.