# Extra Lean documentation

* The [conversion tactic mode](extras/conv.md)
* The [simplifier](extras/simp.md)
* The [calc environment](extras/calc.md)
* The [congruence closure tactic](extras/cc.md)
* [Well founded recursion](extras/well_founded_recursion.md)
* A [Tactic writing tutorial](extras/tactic_writing.md)
