Commit 2020-03-16 17:51 42b92aaa

View on Github →

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