git.iko.soy/Idris-dev
on master help sign in
add links between sections
commit25af56b26b6af23c9b19a12af7cbc9b64bdf1e60 authormartinbaker <git29f185@martinb.com> dateSun 15 Dec 2019, 09:45 (7 years ago) parent4abb58f
2 files changed+12−2
compare with master
unifiedsplit
docs/elaboratorReflection/elaborator-reflection.rst+6−1 docs/reference/language-extensions.rst+6−1
docs/elaboratorReflection/elaborator-reflection.rst+6−1
@@ -198,7 +198,12 @@ This is primarily useful for code generation, particularly for generating patter
198198
199199Learn More
200200==========
201−Tactics are discussed in the proofs section.
201+
202+Some tactics are introduced in the :ref:`proofs-index` section with further details, of those most relevant to elaborator reflection, on the following pages.
202203
203204The list of built-in tactics can be obtained using the ``:browse`` command in an Idris REPL or the corresponding feature in one of the graphical IDE clients to explore the ``Language.Reflection.Elab.Tactics`` namespace.
204205All of the built-in tactics contain documentation strings.
206+
207+For alternative ways to extend the Idris language see the :ref:`reference-index` section.
208+
209+The following pages explain more about the theory and practice of elaborator reflection.
docs/reference/language-extensions.rst+6−1
@@ -3,7 +3,6 @@ Language Extensions
33*******************
44
55
6−
76Type Providers
87===============
98
@@ -34,3 +33,9 @@ repository <https://github.com/david-christiansen/idris-type-providers>`__.
3433More detailed descriptions are available in David Christiansen's `WGP
3534'13 paper <http://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
3635thesis <http://itu.dk/people/drc/david-christiansen-thesis.pdf>`__.
36+
37+Elaborator Reflection
38+=====================
39+
40+Another way to extend the language is elaborator reflection which is described
41+in the :ref:`elaborator-index` section.