The Pieuvre Proof Assistant

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

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

Note d'implémentation

Répartition du travail

Adrien

• Option typecheck

Samy

Fonctions de manipulation des λ-termes (pieuvre.ml) Typecheck