@@ -32,6 +32,9 @@ Running Elaborator Scripts
33On their own, tactics have no effect.
33On their own, tactics have no effect.
34The meta-operation ``%runElab script`` runs ``script`` in the current elaboration context.
34The 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).
35For example, the following script constructs the identity function at type ``Nat``:
38For example, the following script constructs the identity function at type ``Nat``:
37.. code-block:: idris
40.. code-block:: idris