Merge pull request #4 from kim-em/fix-unused-arguments

fix: add nolint unusedArguments to incomplete definitions

Author: Paul-Lez

PersistentDecomp/DirectSumDecomposition.lean

@@ -211,6 +211,7 @@ variable {D : DirectSumDecomposition M}
 /-- If `D` is a direct sum decomposition of `M` and for each `N` appearing in `D` we are given a
 direct sum decomposition of `N`, we can construct a refinement of `D` whose underlying set is the
 union of all decompositions of the `N`'s appearing in `D`. -/
+@[nolint unusedArguments]
 def refinement (B : ∀ N ∈ D, Set (PersistenceSubmodule M))
     (hB : ∀ N hN, N = sSup (B N hN)) (hB' : ∀ N hN, sSupIndep (B N hN))
     (hB'' : ∀ N hN, ⊥ ∉ B N hN) : DirectSumDecomposition M where

PersistentDecomp/DirectSumDecompositionDual.lean

@@ -294,6 +294,7 @@ variable {D : DirectSumDecomposition M}
 
 /--If `D` is a direct sum decomposition of `M` and for each `N` appearing in `S` we are given a
 direct sum decomposition of `N`, we can construct a refinement of `D`.-/
+@[nolint unusedArguments]
 def refinement (B : ∀ N ∈ D, Set (PersistenceSubmodule M))
     (hB : ∀ N hN, N = sSup (B N hN)) (hB' : ∀ N hN, sSupIndep (B N hN))
     (hB'' : ∀ N hN, ⊥ ∉ B N hN) : DirectSumDecomposition M where

PersistentDecomp/MaximalDecompExists.lean

@@ -59,6 +59,7 @@ notation3:max "M["l"]_[" c "]" => chainBound l c
 
 lemma chainBound_le : M[l] ≤ (Λ I l).val := iInf_le ..
 
+@[nolint unusedArguments]
 noncomputable def limit_elt_mk (hT : IsChain LE.le T) (f : T → PersistenceSubmodule M)
   (h_le : ∀ (I J : T), I ≤ J → f J ≤ f I) (h_mem : ∀ I : T, (f I) ∈ I.val) : (L T) := by
   let f' : (I : T) → (Pone T).obj I := by