@@ -109,9 +109,32 @@ If the goal type turns out to have been the unit type, we fill using the unit co
109109Otherwise, we fail with an error message informing the user that the current goal is not trivial.
110110
111111Additionally, the elaboration state can be dumped into an error message with the ``debug`` tactic.
112−A variant, ``debugMessage``, allows arbitrary strings to be included with the state, allowing for a kind of "``printf`` debuggging" of elaboration scripts.
112+A variant, ``debugMessage``, allows arbitrary messages to be included with the state, allowing for a kind of "``printf`` debuggging" of elaboration scripts.
113+The message format used by ``debugMessage`` is the same for errors produced by the error reflection mechanism, allowing the re-use of the Idris pretty-printer when rendering messages.
113114
115+Changing the Global Context
116+===========================
114117
118+``Elab`` scripts can modify the global context during execution.
119+Just as the Idris elaborator produces auxiliary definitions to implement features such as ``where``-blocks and ``case`` expressions, user elaboration scripts may need to define functions.
120+Furthermore, this allows ``Elab`` reflection to be used to implement features such as type class deriving.
121+The operations ``declareType``, ``defineFunction``, and ``addInstance`` allow ``Elab`` scripts to modify the global context.
122+
123+Using Idris's Features
124+======================
125+
126+The Idris compiler has a number of ways to automate the construction of terms.
127+On its own, the ``Elab`` state and its interactions with the unifier allow implicits to be solved using unification.
128+Additional operations use further features of Idris.
129+In particular, ``resolveTC`` solves the current goal using type class resolution, ``search`` invokes the proof search mechanism, and ``sourceLocation`` finds the context in the original file at which the elaboration script is invoked.
130+
131+
132+Recursive Elaboration
133+=====================
134+
135+The elaboration mechanism can be invoked recursively using the ``runElab`` tactic.
136+This tactic takes a goal type and an elaboration script as arguments and runs the script in a fresh lexical evironment to create an inhabitant of the provided goal type.
137+This is primarily useful for code generation, particularly for generating pattern-matching clauses, where variable scope needs to be one that isn't the present local context.
115138
116139Learn More
117140==========