diff --git a/README.md b/README.md index 79052f8..3b4717f 100644 --- a/README.md +++ b/README.md @@ -36,6 +36,16 @@ L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s' ## Notes d'implémentation +- Les λ-termes à trous sont représentés par leurs fonctions de remplissage. À la liste des λ-termes à mettre dans les trous, on associe le λ-terme complété. + +### Découpage des fichiers + +- `lexer.mll` et `parser.mly` les fichiers pour le parser `ocamlyacc` +- `main.ml` contient le code gérant la ligne de commande, le prompt et l'appel à la librairie. +- `pieuvre.ml` contient toutes les fonctions de manipulation de λ-termes. +- `structs.ml` contient l'ensemble des structures de données, genre λ-terme, environnements, types. +- `tactic.ml` contient la structure de définition des tactiques. + ## Répartition du travail ### Adrien