title: Custom prover tactics in Idris
body: <p>If I understand it correctly (mainly from existence of the <code>applyTactic</code> function), it is possible to write custom tactics for the theorem prover in Idris. What (or where) are some examples I could use for learning how to do that?</p>