mathlib3
docs(extras/tactic_writing): add ``%%`(n)`` to the tactic writing guide
#786
Merged
Merged
docs(extras/tactic_writing): add ``%%`(n)`` to the tactic writing guide #786
PatrickMassot
merged
3 commits into
master
from
quotation-docs
add ``%%`(n)`` to the tactic writing guide
e82a457e
PatrickMassot
commented
on 2019-03-03
fix(doc/extras/tactic_writing): propose different idiom for reflectin…
1b0529ca
Merge branch 'master' into quotation-docs
a0a78878
Reviewers
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Login to write a write a comment.
Login via GitHub