@@ -38,11 +38,13 @@ The meta-operation ``%runElab script`` runs ``script`` in the current elaboratio
38For example, the following script constructs the identity function at type ``Nat``:
38For example, the following script constructs the identity function at type ``Nat``:
40.. code-block:: idris
40.. code-block:: idris
41 idNat : Nat -> Nat
42 idNat : Nat -> Nat
42 idNat = %runElab (do intro (Just (UN "x"))
43 idNat = %runElab (do intro (Just (UN "x"))
43 fill (Var (UN "x"))
44 fill (Var (UN "x"))
46On the right-hand side, the Idris elaborator has the goal ``Nat -> Nat``.
48On the right-hand side, the Idris elaborator has the goal ``Nat -> Nat``.
47When it encounters the ``%runElab`` directive, it fulfills this goal by running the provided script.
49When it encounters the ``%runElab`` directive, it fulfills this goal by running the provided script.
48The first tactic, ``intro``, constructs a lambda that binds the name ``x``.
50The 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.
56We can generate identity functions at any concrete type using the same script:
58We can generate identity functions at any concrete type using the same script:
58.. code-block:: idris
60.. code-block:: idris
59 mkId : Elab ()
62 mkId : Elab ()
60 mkId = do intro (Just (UN "x"))
63 mkId = do intro (Just (UN "x"))
61 fill (Var (UN "x"))
64 fill (Var (UN "x"))
@@ -70,6 +73,7 @@ We can generate identity functions at any concrete type using the same script:
70 idString : String -> String
73 idString : String -> String
71 idString = %runElab mkId
74 idString = %runElab mkId
73Interactively Building Elab Scripts
77Interactively Building Elab Scripts
74===================================
78===================================
@@ -99,6 +103,7 @@ The ordinary Idris bind syntax can be used to propagate this information.
99For example, a tactic that solves the current goal when it is the unit type might look like this:
103For example, a tactic that solves the current goal when it is the unit type might look like this:
101.. code-block:: idris
105.. code-block:: idris
102 triv : Elab ()
107 triv : Elab ()
103 triv = do compute
108 triv = do compute
104 g <- getGoal
109 g <- getGoal
@@ -109,6 +114,7 @@ For example, a tactic that solves the current goal when it is the unit type migh
109 , TextPart "is not trivial"
114 , TextPart "is not trivial"
112The tactic ``compute`` normalises the type of its goal with respect to the current context.
118The tactic ``compute`` normalises the type of its goal with respect to the current context.
113While not strictly necessary, this allows ``triv`` to be used in contexts where the triviality of the goal is not immediately apparent.
119While not strictly necessary, this allows ``triv`` to be used in contexts where the triviality of the goal is not immediately apparent.
114Then, ``getGoal`` is used, and its result is bound to ``g``.
120Then, ``getGoal`` is used, and its result is bound to ``g``.