Mysaa/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

README typecheck

Browse Source
This commit is contained in:
Adrien Vannson 2022-05-17 11:26:34 +02:00
parent 425951b1b9
commit bac5f87b4f
No known key found for this signature in database
GPG Key ID: FE2E66FD978C1A55
2 changed files with 9 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
README.md
View File

@ -3,6 +3,13 @@ The Pieuvre Proof Prover
# Presentation # 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 # Note d'implementation
# Répartition du travail # Répartition du travail

3
pieuvre.ml
View File

@ -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 *) (* 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;;