Commit 2020-03-22 17:01 6febc8c0
View on Github →feat(tactic/doc_commands): allow doc strings on add_tactic_doc (#2201)
- feat(tactic/doc_commands): allow doc strings on add_tactic_doc
- Add link to Lean issue.
- Update src/tactic/doc_commands.lean Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
- Change all
description :=to docstrings. - Change suggested by Bryan.
- Use docstrings in library_note
- Factor out
tactic.eval_pexpr. - Add add_decl_doc command.
- Update docs/contribute/doc.md
- Update src/tactic/doc_commands.lean
- Update src/tactic/doc_commands.lean Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com