@@ -37,8 +37,8 @@ For example, the following script constructs the identity function at type ``Nat
37.. code-block:: idris
37.. code-block:: idris
39 idNat : Nat -> Nat
39 idNat : Nat -> Nat
40− idNat = %runElab (do intro (Just (UN "x"))
40+ idNat = %runElab (do intro `{{x}}
41− fill (Var (UN "x"))
41+ fill (Var `{{x}})
@@ -57,8 +57,8 @@ We can generate identity functions at any concrete type using the same script:
57.. code-block:: idris
57.. code-block:: idris
59 mkId : Elab ()
59 mkId : Elab ()
60− mkId = do intro (Just (UN "x"))
60+ mkId = do intro `{{x}}
61− fill (Var (UN "x"))
61+ fill (Var `{{x}})
64 idNat : Nat -> Nat
64 idNat : Nat -> Nat