From: Claudio Sacerdoti Coen Date: Fri, 15 Jun 2018 14:36:37 +0000 (+0200) Subject: Embarassing bug in eta_eq fixed X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=00833b061a468bfda97a1514729d7048f89825ca;p=fireball-separation.git Embarassing bug in eta_eq fixed --- diff --git a/ocaml/simple.ml b/ocaml/simple.ml index c7b9a3a..b1b05ec 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -21,19 +21,6 @@ type t = | L of t ;; -let measure_of_t = - let rec aux acc = function - | V _ -> acc, 0 - | A(b,t1,t2) -> - let acc, m1 = aux acc t1 in - let acc, m2 = aux acc t2 in - (match b with - | `Some b when !b && not (List.memq b acc) -> b::acc, 1 + m1 + m2 - | _ -> acc, m1 + m2) - | L t -> aux acc t - in snd ++ (aux []) -;; - let index_of x = let rec aux n = function @@ -88,6 +75,19 @@ let delta = L(A(`Some (ref true),V 0, V 0));; (* does NOT lift the argument *) let mk_lams = fold_nat (fun x _ -> L x) ;; +let measure_of_t = + let rec aux acc = function + | V _ -> acc, 0 + | A(b,t1,t2) -> + let acc, m1 = aux acc t1 in + let acc, m2 = aux acc t2 in + (match b with + | `Some b when !b && not (List.memq b acc) -> b::acc, 1 + m1 + m2 + | _ -> acc, m1 + m2) + | L t -> aux acc t + in snd ++ (aux []) +;; + type problem = { orig_freshno: int ; freshno : int