3ab5036 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

fix some documentation markup warnings

commit3ab5036ab7fecea7f6c229109860dd47d2084a46 authormartinbaker <git29f185@martinb.com> dateTue 23 Jul 2019, 17:05 (7 years ago) parent9549d9c

2 files changed+4−2

unifiedsplit

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