git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4745 from martinbaker/fixMarkup

fix some documentation markup warnings

commita8d2afcc5d468c2a38423166b5bb3e4dc64c5b70 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateThu 1 Aug 2019, 09:54 (7 years ago) parenta1b30979a7e8d7
3 files changed+5−3
compare with master
unifiedsplit
docs/proofs/interactive.rst+2−2 docs/reference/ffi.rst+2 docs/tutorial/miscellany.rst+1−1
docs/proofs/interactive.rst+2−2
@@ -190,7 +190,7 @@ accessible by pattern matching) and ``ih`` — the local variable
190190containing the result of the recursive call. We can introduce these as
191191assumptions using the ``intro`` tactic twice. The parameter is entered as
192192a constant of type ``TTName`` which is entered as a backtick with double
193−braces `{{ih}}. This gives:
193+braces \`{{ih}}. This gives:
194194
195195.. code-block:: idris
196196
@@ -289,7 +289,7 @@ However if we put the proof into a separate function like this:
289289 plusReducesZ' Z = %runElab (do reflexivity)
290290 plusReducesZ' (S k) = let ih = plusReducesZ' k in plusredZ_S k ih
291291
292−This then loads.
292+This then loads [#f1]_ .
293293
294294.. [#f1] https://github.com/idris-lang/Idris-dev/issues/4556
295295
docs/reference/ffi.rst+2
@@ -121,12 +121,14 @@ Linking foreign code
121121This is the example of linking C code.
122122
123123.. code-block:: idris
124+
124125 %include C "mylib.h"
125126 %link C "mylib.o"
126127
127128Example Makefile
128129
129130.. code-block:: shell
131+
130132 DEFAULT: mylib.o main.idr
131133 idris main.idr -o executableFile
132134
docs/tutorial/miscellany.rst+1−1
@@ -131,7 +131,7 @@ an extension of ``.lidr`` then it is assumed to be a literate file. In
131131literate programs, everything is assumed to be a comment unless the line
132132begins with a greater than sign ``>``, for example:
133133
134−.. code-block:: idris
134+.. code-block:: literate-idris
135135
136136 > module literate
137137