@@ -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,7 @@ 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+Tactics are discussed in the proofs section.
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.
203+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.
204All of the built-in tactics contain documentation strings.