mathlib3
feat(tactic): command for adding tactic, command, and attribute documentation
#2114
Merged
Merged
feat(tactic): command for adding tactic, command, and attribute documentation #2114
mergify
merged
62 commits into
master
from
tactic_doc
chore(*): switch to lean 3.6.0
e6f49012
begin tactic_doc command
aaf1bb1a
merge add_tactic_doc with library_note
eb6aa0a0
fix library_note imports
8e664bba
undo accidental revert
e938161c
better attribute description
4bb1d0eb
unneeded to_expr
ce9f6d09
fix doc string attribution
91df81ea
unicode input error
ce0a0d5d
display and collect doc entries
3bc6e662
missing doc string
7bf907e0
update for lean 3.6
9441b9b2
document core tactics
0c532451
move tfae and rcases docs
4ffa05d3
move rintros and obtain
250d7dd8
simpa
3534e763
move part of tactic.interactive
869d3866
move more of tactic.interactive
7063d2b4
finish tactic.interactive
c3d13d3a
move omega
680eeda8
move renaming tactics
e48c1a9e
move more
cd3d30e8
move norm_cast
55c0e279
more
b2a59fd1
move more
006ea652
doc commands in core + docstring tweaks
daff0a59
abel, alias, cache
9f637fe7
elide, finish
f192b06e
hint, linearith, pi_instances
7a224a7a
norm_num, rewrite
7fae6743
ring, ring_exp
26c6538c
solve_by_elim, suggest
43379dd7
ext
66ac8cc1
explode, find
a8d78f33
lint
6e22b3d8
tidy
908fb456
localized
17e07099
reassoc_axiom, replacer, restate_axiom, where
eb22a1f9
simps
1d350dea
markdown files
1563ebfe
doc_commands, rcases
9f28d5f3
interactive
2632e96a
merge master
c015054f
new additions
3c4a37de
revert changes to md files
e953c91d
fix merge
45236438
allow entries with different categories to share the same name
1a1948f1
better error messages
4c95d82c
gebner
commented
on 2020-03-09
fix merge
bca70c62
linter errors
7c41798e
use derive handler for inhabited instances
6736ad95
shorten doc entry names after category fix
41bae151
copy simp.md to doc entry, tag: "simp" -> "simplification"
674949ff
update add_tactic_doc_command docstring and doc.md
48778abe
bryangingechen
commented
on 2020-03-11
simp doc entry changed to its doc string
56da7b37
bryangingechen
commented
on 2020-03-11
bryangingechen
commented
on 2020-03-11
bryangingechen
commented
on 2020-03-11
bryangingechen
commented
on 2020-03-11
Apply suggestions from code review
57c69be9
doc: horizontal rules must be surrounded by new lines
b7f281cb
Merge branch 'tactic_doc' of github.com:leanprover-community/mathlib …
d7a14646
address reviewer suggestions
c7b25196
Update docs/contribute/doc.md
b836615d
fix add_tactic_doc_command docstring
7966802e
gebner
approved these changes
on 2020-03-16
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into tactic_doc
fa6cd3ca
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub