Add titles to proof docs
Generates proper hierarchy in ToCs and the side-bar. Also avoids
typesetting anomalies when bulleted lists appear before the 1st
section heading.
commit6c2183fb59478af6eaf26b57ed0e4bbe08814a42
authorCraig Ramsay <cramsay01@gmail.com>
dateMon 11 Nov 2019, 14:02 (7 years ago)
parentf3cff28
docs/proofs/definitional.rst+4
@@ -1,3 +1,7 @@
1+*******************
2+Background Material
3+*******************
4+
15In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as,
26
37- Propositions and judgments
docs/proofs/propositional.rst+4−3
@@ -1,7 +1,8 @@
1−This page attempts to explain some of the techniques used in Idris to prove propositional equalities.
2−
1+******************************
32Proving Propositional Equality
4−==============================
3+******************************
4+
5+This page attempts to explain some of the techniques used in Idris to prove propositional equalities.
56
67We have seen that definitional equalities can be proved using Refl since they always normalise to unique values that can be compared directly.
78