chore: remove final use of fin_destr in data macro

alexkeizer · May 20, 2024 · cefe5e6 · cefe5e6
1 parent 47a1a62
commit cefe5e6
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean
@@ -15,7 +15,6 @@ open PrettyPrinter (delab)
 private def Array.enum (as : Array α) : Array (Nat × α) :=
   (Array.range as.size).zip as
 
-
 /--
   Given a natural number `n`, produce a sequence of `n` calls of `.fs`, ending in `.fz`.
 
@@ -303,7 +302,8 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
         cases head
         <;> simp
         <;> apply congrArg
-        <;> fin_destr
+        <;> (funext i; fin_cases i)
+        <;> (funext (j : PFin2 _); fin_cases j)
         <;> rfl
 
     instance $functor:ident : MvFunctor (@TypeFun.ofCurried $(quote arity) $shape) where