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.

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é.

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.

Option `typecheck`

L'option typecheck peut être testée avec les fichiers tests dans tests/typecheck. Pour cela, utiliser les commandes :

./pieuvre -typecheck tests/typecheck/right-type
./pieuvre -typecheck tests/typecheck/wrong-type

Option `alpha`

L'option alpha vérifie si deux lambda-termes sont alpha-équivalents. Elle s'utilise de la manière suivante :

./pieuvre -alpha tests/lambda-terms/alpha-eq.lams
./pieuvre -alpha tests/lambda-terms/alpha-not-eq.lams

Option `reduce`

L'option alpha vérifie si deux lambda-termes sont alpha-équivalents. Elle s'utilise de la manière suivante :

./pieuvre -reduce tests/lambda-terms/lambda.lam

Notes d'implémentation

Répartition du travail

Adrien

Option typecheck

Samy

Fonctions de manipulation des λ-termes (pieuvre.ml) Typecheck Erreurs lors des tactiques. / et /\

README.md

The Pieuvre™ Proof Assistant