Commit 2022-06-23 18:33 20c6d70b

View on Github →

chore: fix unused variables from linter (#289) This makes mathlib pass the new unused variables linter added to lean 4 core.

Estimated changes

modified theorem Fin.size_positive
modified theorem List.drop_eq_nil_of_le
modified theorem List.get?_append_right
modified theorem List.mem_or_eq_of_mem_set
modified theorem List.set_comm
modified def List.takeD
modified theorem List.Perm.swap'
modified theorem List.perm_insertNth
modified theorem Int.nonneg_or_nonneg_neg
modified theorem List.subset.refl
modified theorem List.subset_cons
modified theorem Nat.add_mod
modified theorem Nat.add_mod_mod
modified def Nat.discriminate
modified theorem Nat.dvd_of_mod_eq_zero
modified theorem Nat.nat_repr_len_aux
modified theorem Nat.repr_length
modified theorem Nat.to_digits_core_length
modified theorem Nat.to_digits_core_lens_eq
modified def Decidable.by_cases
modified theorem if_congr_prop
modified def Set.univ
modified def decidable_of_bool
modified def decidable_of_iff'
modified def decidable_of_iff
modified theorem exists_false
modified theorem exists_prop
modified theorem Function.const_def
modified theorem exists_true_iff_nonempty
modified def SlimCheck.NamedBinder