@@ -38,11 +38,13 @@ The meta-operation ``%runElab script`` runs ``script`` in the current elaboratio
3838For example, the following script constructs the identity function at type ``Nat``:
3939
4040.. code-block:: idris
41+
4142 idNat : Nat -> Nat
4243 idNat = %runElab (do intro (Just (UN "x"))
4344 fill (Var (UN "x"))
4445 solve)
4546
47+
4648On the right-hand side, the Idris elaborator has the goal ``Nat -> Nat``.
4749When it encounters the ``%runElab`` directive, it fulfills this goal by running the provided script.
4850The first tactic, ``intro``, constructs a lambda that binds the name ``x``.
@@ -56,6 +58,7 @@ Note that there is nothing ``Nat``-specific about the above script.
5658We can generate identity functions at any concrete type using the same script:
5759
5860.. code-block:: idris
61+
5962 mkId : Elab ()
6063 mkId = do intro (Just (UN "x"))
6164 fill (Var (UN "x"))
@@ -70,6 +73,7 @@ We can generate identity functions at any concrete type using the same script:
7073 idString : String -> String
7174 idString = %runElab mkId
7275
76+
7377Interactively Building Elab Scripts
7478===================================
7579
@@ -99,6 +103,7 @@ The ordinary Idris bind syntax can be used to propagate this information.
99103For example, a tactic that solves the current goal when it is the unit type might look like this:
100104
101105.. code-block:: idris
106+
102107 triv : Elab ()
103108 triv = do compute
104109 g <- getGoal
@@ -109,6 +114,7 @@ For example, a tactic that solves the current goal when it is the unit type migh
109114 , TextPart "is not trivial"
110115 ]
111116
117+
112118The tactic ``compute`` normalises the type of its goal with respect to the current context.
113119While not strictly necessary, this allows ``triv`` to be used in contexts where the triviality of the goal is not immediately apparent.
114120Then, ``getGoal`` is used, and its result is bound to ``g``.