Def mkDocComment

Modification history

2026-01-13 15:36
MathlibTest/willRoundTrip.lean
fix(Tactic/Widget/Conv): fix various issues (#25889) …
Added mkDocCommentView on Github →