git.iko.soy/Idris-dev
on master help sign in
changes to tactics.rst
543a382Martin Baker
docs/proofs/tactics.rst+7−15
compare with master
unifiedsplit
@@ -81,21 +81,17 @@ Quasiquotation
81
81
82Since names are used frequently in elaborator reflection there is a shortcut for constructing them:
82Since names are used frequently in elaborator reflection there is a shortcut for constructing them:
83
83
84−.. list-table:: Quasiquotation
84+.. list-table::
85
85
86 * - An unresolved variable "x" is wrapped in backtick and double braces:
86 * - An unresolved variable "x" is wrapped in backtick and double braces:
87− - example
88−
89− .. code-block:: idris
87+ - .. code-block:: idris
90
88
91 Idris> `{{x}}
89 Idris> `{{x}}
92 UN "x" : TTName
90 UN "x" : TTName
93
91
94
92
95 * - Single braces are used for existing variables:
93 * - Single braces are used for existing variables:
96− - example
97−
98− .. code-block:: idris
94+ - .. code-block:: idris
99
95
100 Idris> `{x}
96 Idris> `{x}
101 No such variable x
97 No such variable x
@@ -105,9 +101,9 @@ Since names are used frequently in elaborator reflection there is a shortcut for
105
101
106
102
107 * - brackets are used for an expression:
103 * - brackets are used for an expression:
108− - example here type is inferable
109
104
105+ here type is inferable
110− .. code-block:: idris
106+ - .. code-block:: idris
111
107
112 Idris> :let a=2
108 Idris> :let a=2
113 Idris> `(a)
109 Idris> `(a)
@@ -115,18 +111,14 @@ Since names are used frequently in elaborator reflection there is a shortcut for
115
111
116
112
117 * - Expression with explicit type:
113 * - Expression with explicit type:
118− - example
119−
120− .. code-block:: idris
114+ - .. code-block:: idris
121
115
122 Idris> `(a:Integer)
116 Idris> `(a:Integer)
123 P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
117 P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
124
118
125
119
126 * - If we want the value we can escape from quasiquotation by using anti-quotation (tilde)
120 * - 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
130
122
131 Idris> `(~a)
123 Idris> `(~a)
132 2 : Integer
124 2 : Integer