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.

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

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

Note d'implémentation

Répartition du travail

Adrien

Samy

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