Commit 2022-11-20 21:24 d419b094

View on Github →

chore: fix linter warnings in tests (#662)

Estimated changes

Modified lean_packages/manifest.json

Modified test/Clear!.lean

Modified test/ClearExcept.lean

Modified test/Clear_.lean

Modified test/Have.lean

Modified test/PermuteGoals.lean

Modified test/Replace.lean

Modified test/Set.lean

Modified test/Simps.lean

Modified test/SolveByElim.lean

Modified test/basicTactics.lean

Modified test/congr.lean

Modified test/irreducibleDef.lean

Modified test/librarySearch.lean

modified theorem lemma_with_false_in_head

Modified test/positivity.lean