Commit 2022-10-24 03:11 db2b67f7

View on Github →

feat: port copy_doc_string command (#494)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/DocCommands.lean

Created test/DocCommands.lean

added def hi

added def one

added def three

added def two