From 704fd9d9db0c01619264527d4174afe74bdff53d Mon Sep 17 00:00:00 2001 From: acondolu Date: Mon, 24 Jul 2017 13:09:05 +0200 Subject: [PATCH] Fixed eta_compare in the case Lam vs. Bot --- ocaml/num.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ocaml/num.ml b/ocaml/num.ml index 1e630f4..aa9338c 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -295,8 +295,8 @@ let eta_compare x y = | `Pacman, `Pacman -> 0 | `Lam _, `N _ -> -1 | `N _, `Lam _ -> 1 - | `Bottom, `Lam(_,t) -> prerr_endline "(* TO BE UNDERSTOOD *)"; aux `Bottom t - | `Lam(_,t), `Bottom -> prerr_endline "(* TO BE UNDERSTOOD *)"; aux t `Bottom + | `Bottom, `Lam(_,t) -> -1 + | `Lam(_,t), `Bottom -> 1 | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2 | `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666))) | t2, `Lam(_,t1) -> aux t1 (mk_app (lift 1 t2) (`Var(0,-666))) -- 2.39.2