git.iko.soy/Idris-dev
on master help sign in
fix duplicate name
4abb58fmartinbaker
docs/elaboratorReflection/index.rst+5−11
compare with master
unifiedsplit
@@ -1,8 +1,8 @@
1−.. _proofs-index:
1+.. _elaborator-index:
2
2
3−#########################################
3+#####################
4−Theorem Proving and Elaborator Reflection
4+Elaborator Reflection
5−#########################################
5+#####################
6
6
7A tutorial on theorem proving in Idris.
7A tutorial on theorem proving in Idris.
8
8
@@ -18,13 +18,7 @@ A tutorial on theorem proving in Idris.
18.. toctree::
18.. toctree::
19 :maxdepth: 1
19 :maxdepth: 1
20
20
21− definitional
21+ elaborator-reflection
22− pluscomm
23− inductive
24− patterns
25− propositional
26− interactive
27− interactiveOld
28 elabReflection
22 elabReflection
29 tactics
23 tactics
30 holes
24 holes