diff --git a/README.md b/README.md index 0ace960..6aa8d7f 100644 --- a/README.md +++ b/README.md @@ -3,6 +3,13 @@ The Pieuvre Proof Prover # Presentation +## 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'implementation # Répartition du travail diff --git a/pieuvre.ml b/pieuvre.ml index 1e8c8c2..8182c56 100644 --- a/pieuvre.ml +++ b/pieuvre.ml @@ -234,4 +234,5 @@ let rec computeType (env: gam) (l: lam) : ty option = ;; (* Vérifie que le λ-terme l sous l'environnement env a bien le type t *) -let typecheck (env: gam) (l: lam) (t: ty) : bool = (computeType env l = Some t); +let typecheck (env: gam) (l: lam) (t: ty) : bool = + computeType env l = Some t;;