@@ -1,8 +1,8 @@
11.. _elaborator-reflection:
22
3−*********************
4−Elaborator Reflection
5−*********************
3+**********************************
4+Elaborator Reflection Introduction
5+**********************************
66
77The Idris elaborator is responsible for converting high-level Idris code into the core language.
88It 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
198198
199199Learn More
200200==========
201−While this documentation is still incomplete, elaboration reflection works in Idris today.
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.
201+Tactics are discussed in the proofs section.
202+
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.
203204All of the built-in tactics contain documentation strings.