Def Mathlib.Util.LibraryNote.getDocCommentContent

Modification history

2022-09-04 16:26
Mathlib/Util/LibraryNote.lean
feat: depend on std4 (#397)
Deleted Mathlib.Util.LibraryNote.getDocCommentContentView on Github →
2022-02-07 19:05
Mathlib/Util/LibraryNote.lean
feat: library_note (#188)
Added Mathlib.Util.LibraryNote.getDocCommentContentView on Github →