git.iko.soy/Idris-dev
on master help sign in
Add titles to proof docs
6c2183fCraig Ramsay
docs/proofs/definitional.rst+4
compare with master
unifiedsplit
@@ -1,3 +1,7 @@
1+*******************
2+Background Material
3+*******************
4+
1In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as,
5In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as,
2
6
3- Propositions and judgments
7- 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.
1+******************************
2−
3Proving Propositional Equality
2Proving Propositional Equality
4−==============================
3+******************************
4+
5+This page attempts to explain some of the techniques used in Idris to prove propositional equalities.
5
6
6We have seen that definitional equalities can be proved using Refl since they always normalise to unique values that can be compared directly.
7We have seen that definitional equalities can be proved using Refl since they always normalise to unique values that can be compared directly.
7
8