Theorem ProvingΒΆ
A tutorial on theorem proving in Idris.
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/
- Propositions and Judgments
- Curry-Howard correspondence
- Definitional and Propositional Equalities
- Axiomatic and Constructive Approaches
- Running example: Addition of Natural Numbers
- Inductive Proofs
- Pattern Matching Proofs
- Proving Propositional Equality
- Replace
- Rewrite
- Symmetry and Transitivity
- Heterogeneous Equality
- Interactive Theorem Proving
- DEPRECATED: Interactive Theorem Proving Using Old Tactics Code