mathlib

42b92aaa - feat(tactic): command for adding tactic, command, and attribute documentation (#2114)

feat(tactic): command for adding tactic, command, and attribute documentation (#2114) * chore(*): switch to lean 3.6.0 * begin tactic_doc command * merge add_tactic_doc with library_note * fix library_note imports * undo accidental revert * better attribute description * unneeded to_expr * fix doc string attribution * unicode input error Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * display and collect doc entries * missing doc string * update for lean 3.6 * document core tactics I considered adding these as doc strings in core. But the entry for `conv` mentions mathlib-specific things. * move tfae and rcases docs * move rintros and obtain * simpa * move part of tactic.interactive * move more of tactic.interactive * finish tactic.interactive * move omega * move renaming tactics * move more * move norm_cast * more * move more * doc commands in core + docstring tweaks * abel, alias, cache * elide, finish * hint, linearith, pi_instances * norm_num, rewrite * ring, ring_exp * solve_by_elim, suggest * doc_commands, rcases * ext * explode, find * lint * tidy * localized * reassoc_axiom, replacer, restate_axiom, where * simps * markdown files * interactive * new additions * revert changes to md files * fix merge * allow entries with different categories to share the same name * better error messages * fix merge * linter errors * use derive handler for inhabited instances * shorten doc entry names after category fix * copy simp.md to doc entry, tag: "simp" -> "simplification" * update add_tactic_doc_command docstring and doc.md * simp doc entry changed to its doc string * Apply suggestions from code review * doc: horizontal rules must be surrounded by new lines * address reviewer suggestions * Update docs/contribute/doc.md Co-Authored-By: Gabriel Ebner <gebner@gebner.org> * fix add_tactic_doc_command docstring Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>