git.iko.soy/Idris-dev
on master help sign in
add links between sections
25af56bmartinbaker
docs/elaboratorReflection/elaborator-reflection.rst+6−1
compare with master
unifiedsplit
@@ -198,7 +198,12 @@ This is primarily useful for code generation, particularly for generating patter
198
198
199Learn More
199Learn More
200==========
200==========
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.
202
203
203The 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.
204The 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.
204All of the built-in tactics contain documentation strings.
205All 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
3*******************
3*******************
4
4
5
5
6−
7Type Providers
6Type Providers
8===============
7===============
9
8
@@ -34,3 +33,9 @@ repository <https://github.com/david-christiansen/idris-type-providers>`__.
34More detailed descriptions are available in David Christiansen's `WGP
33More detailed descriptions are available in David Christiansen's `WGP
35'13 paper <http://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
34'13 paper <http://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
36thesis <http://itu.dk/people/drc/david-christiansen-thesis.pdf>`__.
35thesis <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.