@@ -81,21 +81,17 @@ Quasiquotation
8181
8282Since names are used frequently in elaborator reflection there is a shortcut for constructing them:
8383
84−.. list-table:: Quasiquotation
84+.. list-table::
8585
8686 * - An unresolved variable "x" is wrapped in backtick and double braces:
87− - example
88−
89− .. code-block:: idris
87+ - .. code-block:: idris
9088
9189 Idris> `{{x}}
9290 UN "x" : TTName
9391
9492
9593 * - Single braces are used for existing variables:
96− - example
97−
98− .. code-block:: idris
94+ - .. code-block:: idris
9995
10096 Idris> `{x}
10197 No such variable x
@@ -105,9 +101,9 @@ Since names are used frequently in elaborator reflection there is a shortcut for
105101
106102
107103 * - brackets are used for an expression:
108− - example here type is inferable
109104
110− .. code-block:: idris
105+ here type is inferable
106+ - .. code-block:: idris
111107
112108 Idris> :let a=2
113109 Idris> `(a)
@@ -115,18 +111,14 @@ Since names are used frequently in elaborator reflection there is a shortcut for
115111
116112
117113 * - Expression with explicit type:
118− - example
119−
120− .. code-block:: idris
114+ - .. code-block:: idris
121115
122116 Idris> `(a:Integer)
123117 P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
124118
125119
126120 * - If we want the value we can escape from quasiquotation by using anti-quotation (tilde)
127− - example
128−
129− .. code-block:: idris
121+ - .. code-block:: idris
130122
131123 Idris> `(~a)
132124 2 : Integer