Commit 2022-02-07 19:05 d54e4e1a

View on Github →

feat: library_note (#188)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic/Lint/Simp.lean

Created Mathlib/Util/LibraryNote.lean

added def Mathlib.Util.LibraryNote.LibraryNoteEntry

added def Mathlib.Util.LibraryNote.getDocCommentContent