df9c178 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fixes build errors relating to use of Sphinx 1.2.2.

Some minor warnings still remain but they seem minor and non-important.

commitdf9c178131c066f954ad8c7901de21e5e14899e2 authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateTue 24 Mar 2015, 09:21 (12 years ago) parentaf1569c

6 files changed+14−12

compare with master

unifiedsplit

docs/effects/simpleeff.rst+1−2 docs/index.rst+1−1 docs/tutorial/interp.rst+2−1 docs/tutorial/modules.rst+4−2 docs/tutorial/starting.rst+1−1 docs/tutorial/typesfuns.rst+5−5

docs/effects/simpleeff.rst+1−2

@@ -274,8 +274,7 @@ correct:

274274

275275 guess : Int -> { [STDIO] } Eff ()

276276

277−For reference, the code for ``guess`` is given in Listing

278−:ref:`eff-game`.

277+For reference, the code for ``guess`` is given below:

279278

280279.. _eff-game:

281280.. code-block:: idris

docs/index.rst+1−1

@@ -64,7 +64,7 @@ Learning Effects

6464 effects/conclusions

6565 effects/summary

6666

67−.. _proofs::

67+.. _proofs:

6868

6969###############

7070Theorem Proving

docs/tutorial/interp.rst+2−1

@@ -266,8 +266,9 @@ integer, giving 0 if the input is invalid. An example run of this

266266program at the Idris interactive environment is:

267267

268268

269+.. _factrun:

269270.. literalinclude:: ../listing/idris-prompt-interp.txt

270− :name: factrun

271+

271272

272273Aside: ``cast``

273274~~~~~~~~~~~~~~~

docs/tutorial/modules.rst+4−2

@@ -10,7 +10,7 @@ module, a list of ``import`` statements giving the other modules which

1010are to be imported, and a collection of declarations and definitions of

1111types, classes and functions. For example, the listing below gives a

1212module which defines a binary tree type ``BTree`` (in a file

13−``btree.idr``):;

13+``btree.idr``):

1414

1515.. code-block:: idris

1616

@@ -32,8 +32,9 @@ module which defines a binary tree type ``BTree`` (in a file

3232 toTree [] = Leaf

3333 toTree (x :: xs) = insert x (toTree xs)

3434

35+

3536Then, this gives a main program (in a file

36−``bmain.idr``) which uses the ``bst`` module to sort a list::

37+``bmain.idr``) which uses the ``bst`` module to sort a list:

3738

3839.. code-block:: idris

3940

@@ -45,6 +46,7 @@ Then, this gives a main program (in a file

4546 main = do let t = toTree [1,8,2,7,9,3]

4647 print (btree.toList t)

4748

49+

4850The same names can be defined in multiple modules. This is possible

4951because in practice names are *qualified* with the name of the module.

5052The names defined in the ``btree`` module are, in full:

docs/tutorial/starting.rst+1−1

@@ -86,5 +86,5 @@ checking a file, if successful, creates a bytecode version of the file

8686(in this case ``hello.ibc``) to speed up loading in future. The

8787bytecode is regenerated if the source file changes.

8888

89+.. _run1:

8990.. literalinclude:: ../listing/idris-prompt-helloworld.txt

90− :name: run1

docs/tutorial/typesfuns.rst+5−5

@@ -221,8 +221,8 @@ declaration for a function ``f`` *can* be omitted if:

221221

222222- ``f`` appears in the right hand side of the top level definition

223223

224−- The type of ``f`` can be completely determined from its first

225− application

224+- The type of ``f`` can be completely determined from its first application

225+

226226

227227So, for example, the following definitions are legal:

228228

@@ -948,10 +948,10 @@ analysis of intermediate expressions to avoid the need to write

948948auxiliary functions, and is also used internally to implement pattern

949949matching ``let`` and lambda bindings. It will *only* work if:

950950

951−- Each branch *matches* a value of the same type, and *returns* a value

952− of the same type.

951+- Each branch *matches* a value of the same type, and *returns* a

952+ value of the same type.

953953

954−- The type of the result is “known”. i.e. the type of the expression

954+- The type of the result is "known". i.e. the type of the expression

955955 can be determined *without* type checking the ``case``-expression

956956 itself.

957957