]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Step possible beyond the args of p.div
authoracondolu <andrea.condoluci@unibo.it>
Sun, 10 Jun 2018 14:49:49 +0000 (16:49 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Sun, 10 Jun 2018 14:49:49 +0000 (16:49 +0200)
ocaml/simple.ml

index 60b4e8779f4aa41705dd8016fd3c2918599a74da..079774e5ac67e5c53feaa53eca9e7e622dd77c76 100644 (file)
@@ -257,9 +257,11 @@ let inert_cut_at n t =
 let find_eta_difference p t =\r
  let divargs = args_of_inert p.div in\r
  let conargs = args_of_inert t in\r
+ let rec range i j =\r
+  if j = -1 then [] else i :: range (i+1) (j-1) in\r
  let rec aux k divargs conargs =\r
   match divargs,conargs with\r
-     [],_ -> []\r
+     [],conargs -> range k (List.length conargs)\r
    | _::_,[] -> [k]\r
    | t1::divargs,t2::conargs ->\r
       (if not (eta_eq t1 t2) then [k] else []) @ aux (k+1) divargs conargs\r