Correction du typage de ExFalso.
This commit is contained in:
parent
188bc43576
commit
2b98fd6407
@ -137,9 +137,9 @@ let rec computeType (env: gam) (l: lam) : ty option =
|
|||||||
| [] -> None
|
| [] -> None
|
||||||
end
|
end
|
||||||
| LExf(l',t) ->
|
| LExf(l',t) ->
|
||||||
if (computeType env l')=Some t
|
match (computeType env l') with
|
||||||
then Some t
|
| Some TFalse -> Some t (* On applique le ExFalso *)
|
||||||
else None (* Le ex falso a le mauvais type *)
|
| _ -> None (* Le ex falso a le mauvais type *)
|
||||||
;;
|
;;
|
||||||
|
|
||||||
(* 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 *)
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user