@@ -37,8 +37,8 @@ For example, the following script constructs the identity function at type ``Nat
3737.. code-block:: idris
3838
3939 idNat : Nat -> Nat
40− idNat = %runElab (do intro (Just (UN "x"))
41− fill (Var (UN "x"))
40+ idNat = %runElab (do intro `{{x}}
41+ fill (Var `{{x}})
4242 solve)
4343
4444
@@ -57,8 +57,8 @@ We can generate identity functions at any concrete type using the same script:
5757.. code-block:: idris
5858
5959 mkId : Elab ()
60− mkId = do intro (Just (UN "x"))
61− fill (Var (UN "x"))
60+ mkId = do intro `{{x}}
61+ fill (Var `{{x}})
6262 solve
6363
6464 idNat : Nat -> Nat