doc: T-Lam

README.md

@@ -280,19 +280,32 @@ Autrement dit, si l'on peut caster une classe $A$ vers une autre classe $B$, alo
 
 Si l'on définit une méthode `mtype`prenant en paramètre le nom d'une méthode ($m$) et la classe/interface associée ($T_0$), et qui renvoie la liste des types de ses paramètres associée $\overline{U}$ son type de retour $T$,
 et si dans notre environnement, il existe une expression $e_0$, que l'on peut caster en $e_0'$ en l'annotatant du type $T_0$,
-et que les paramètres $\overline{e}$ de cette méthode $m$ peuvent être castés par $\overline{U}$ avec $\lambda$`-mark`, en produisant une nouvelle liste $\overline{e'}$ de paramètres,
+et que les paramètres $\overline{e}$ de cette méthode $m$ peuvent être castés par $\overline{U}$ avec $\lambda$`mark`, en produisant une nouvelle liste $\overline{e'}$ de paramètres,
 et que si dans notre environnement, cette nouvelle liste peut être associée à une nouvelle liste $\overline{e''}$ d'argument annotés par une liste de type $\overline{T}$, qui sont des sous-types de $\overline{U}$ ;
 
 Alors, la méthode $m$ peut être appelée avec des paramètres castés si ces paramètres sont d'un type qui étend le type des paramètres d'origine 
-(après que ces attributs aient été annotés pas $\lambda$`-mark`).
+(après que ces attributs aient été annotés pas $\lambda$`mark`).
 
 ##### `T-New`
 
-Après que les attributs (de type $\overline{U}$) d'une classe ait été annotés par $\lambda$`-mark`, 
+Après que les attributs (de type $\overline{U}$) d'une classe ait été annotés par $\lambda$`mark`, 
 si l'on note que ces nouveaux attributs annotés peuvent être castés en un autre sous type ($\overline{T}$) ;
 
 Alors, un constructeur peut être appelé avec des paramètres castés si ces paramètres sont d'un type qui étend le type des paramètres d'origine
 
+##### `T-Lam` *Comment typer une $\lambda$-expression$*
+
+Si l'on a pu caster une expression $e$ en une interface (i.e. associer $e$ à $e'$, par l'annotation d'une interface), 
+et que l'interface en question n'est constituée que d'une seule méthode abstraite ;
+
+Alors cette expression implémente une interface fonctionnelle.
+
+Si une expression implémente une interface fonctionnelle, 
+et que l'on peut y appliquer $\lambda$`mark` sur le corps de sa méthode, produisant ainsi une nouvelle expression $e''$,
+et que cette nouvelle expression peut être jugée en tant que sous type de l'expression $e'$ ;
+
+Alors, l'expression $e$ est une $\lambda$-expression$
+
 #### Règles de réduction
 
 ### FJ vs Java