Def mkDocComment

Modification history

2026-10-18 09:39
MathlibTest/willRoundTrip.lean
chore(MathlibTest): remove `mkDocComment` (#44972) …
Deleted mkDocCommentView on Github →
2026-01-13 15:36
MathlibTest/willRoundTrip.lean
fix(Tactic/Widget/Conv): fix various issues (#25889) …
Added mkDocCommentView on Github →