fix(frontends/lean/elaborator): use_elim_elab_core

library/init/wf.lean

@@ -58,10 +58,7 @@ namespace well_founded
 
   theorem fix_F_eq (x : A) (r : acc R x) :
     fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)) :=
-  @acc.drec A R
-    (λ x r, fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)))
-    (λ x r ih, rfl)
-    x r
+  acc.drec (λ x r ih, rfl) r
   end
 
   variables {A : Type u} {C : A → Type v} {R : A → A → Prop}

src/frontends/lean/elaborator.cpp

@@ -327,7 +327,6 @@ auto elaborator::use_elim_elab_core(name const & fn) -> optional<elim_info> {
                 found[*pos] = true;
                 idxs.push_back(i);
             }
-            continue;
         }
 
         expr param_type = m_ctx.infer(param);