@@ -32,6 +32,9 @@ Running Elaborator Scripts
3232
3333On their own, tactics have no effect.
3434The meta-operation ``%runElab script`` runs ``script`` in the current elaboration context.
35+Before you can use ``%runElab``, you will have to enable the language extension by adding
36+``%language ElabReflection`` in your file (or by passing ``-X ElabReflection`` to the
37+``idris`` executable from your command line).
3538For example, the following script constructs the identity function at type ``Nat``:
3639
3740.. code-block:: idris