mathlib
bda8a050 - doc(docs/extras/tactic_writing) add cheap method (#2198)

Commit
5 years ago
doc(docs/extras/tactic_writing) add cheap method (#2198) * doc(docs/extras/tactic_writing) add cheap method About 50% of my personal use cases for writing tactics are just because I want a simple way of stringing several tactics together, so I propose adding this so I will know where to look when I realise I can't remember the syntax. * style fixes * Update tactic_writing.md * Update tactic_writing.md * Update docs/extras/tactic_writing.md Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading