mathlib3
bc40b44c - doc(tactic/doc_commands): fix doc comment (#15947)

Commit

3 years ago

doc(tactic/doc_commands): fix doc comment (#15947) As noted at https://github.com/leanprover-community/mathlib/pull/15913#discussion_r940698781 .

Author

digama0

Parents