a8d2afc · Idris-dev · git.iko.soy

docs/proofs/interactive.rst+2−2

compare with master

unifiedsplit

@@ -190,7 +190,7 @@ accessible by pattern matching) and ``ih`` — the local variable

190containing the result of the recursive call. We can introduce these as

191assumptions using the ``intro`` tactic twice. The parameter is entered as

192a constant of type ``TTName`` which is entered as a backtick with double

193−braces `{{ih}}. This gives:

193+braces \`{{ih}}. This gives:

194

195.. code-block:: idris

196

@@ -289,7 +289,7 @@ However if we put the proof into a separate function like this:

289 plusReducesZ' Z = %runElab (do reflexivity)

290 plusReducesZ' (S k) = let ih = plusReducesZ' k in plusredZ_S k ih

291

292−This then loads.

292+This then loads [#f1]_ .

293

294.. [#f1] https://github.com/idris-lang/Idris-dev/issues/4556

295

docs/reference/ffi.rst+2

@@ -121,12 +121,14 @@ Linking foreign code

121This is the example of linking C code.

122

123.. code-block:: idris

124+

124 %include C "mylib.h"

125 %include C "mylib.h"

125 %link C "mylib.o"

126 %link C "mylib.o"

126

127

127Example Makefile

128Example Makefile

128

129

129.. code-block:: shell

130.. code-block:: shell

131+

130 DEFAULT: mylib.o main.idr

132 DEFAULT: mylib.o main.idr

131 idris main.idr -o executableFile

133 idris main.idr -o executableFile

132

134

docs/tutorial/miscellany.rst+1−1

@@ -131,7 +131,7 @@ an extension of ``.lidr`` then it is assumed to be a literate file. In

131literate programs, everything is assumed to be a comment unless the line

132begins with a greater than sign ``>``, for example:

133

134−.. code-block:: idris

134+.. code-block:: literate-idris

135

136 > module literate

137