.. _proofs-index: ###############Theorem Proving############### A tutorial on theorem proving in Idris 2.  .. note::    The documentation for Idris has been published under the Creative   Commons CC0 License. As such to the extent possible under law, *The   Idris Community* has waived all copyright and related or neighboring   rights to Documentation for Idris.    More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/ .. toctree::   :maxdepth: 1    definitional   pluscomm   inductive   patterns   propositional