Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-18 06:01 12075180

View on Github →

feat(*): add command for declaring library notes (#1810)

feat(*): add command for declaring library notes
add missing file
make note names private
update docs
Update library_note.lean
Update library_note.lean

Estimated changes

Modified docs/tactics.md

Modified src/algebra/category/Mon/basic.lean

Modified src/algebra/group/hom.lean

Modified src/algebra/module.lean

Modified src/category_theory/limits/preserves.lean

Modified src/group_theory/coset.lean

Modified src/logic/basic.lean

Modified src/meta/expr.lean

Modified src/tactic/core.lean

Created src/tactic/library_note.lean

added def string.hash

Modified src/tactic/lint.lean

Modified src/tactic/localized.lean

deleted def string_hash