Commit 2026-10-18 09:39 d6b19107

View on Github →

chore(MathlibTest): remove mkDocComment (#44972) Remove mkDocComment from MathlibTest/willRoundTrip.lean, which is unused since #44879.

Estimated changes

deleted def mkDocComment