@@ -1,8 +1,8 @@
1.. _elaborator-reflection:
1.. _elaborator-reflection:
3−*********************
3+**********************************
4−Elaborator Reflection
4+Elaborator Reflection Introduction
5−*********************
5+**********************************
7The Idris elaborator is responsible for converting high-level Idris code into the core language.
7The Idris elaborator is responsible for converting high-level Idris code into the core language.
8It is implemented as a kind of embedded tactic language in Haskell, where tactic scripts are written in an *elaboration monad* that provides error handling and a proof state.
8It is implemented as a kind of embedded tactic language in Haskell, where tactic scripts are written in an *elaboration monad* that provides error handling and a proof state.
@@ -198,6 +198,12 @@ This is primarily useful for code generation, particularly for generating patter
199Learn More
199Learn More
200==========
200==========
201−While this documentation is still incomplete, elaboration reflection works in Idris today.
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−As you wait for the completion of the documentation, the 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.
204+The 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.
203All of the built-in tactics contain documentation strings.
205All of the built-in tactics contain documentation strings.
207+For alternative ways to extend the Idris language see the :ref:`reference-index` section.
209+The following pages explain more about the theory and practice of elaborator reflection.