df9c178 · Idris-dev · git.iko.soy

docs/effects/simpleeff.rst+1−2

compare with master

unifiedsplit

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

274

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

276

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

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

278−:ref:`eff-game`.

279

278

280.. _eff-game:

279.. _eff-game:

281.. code-block:: idris

280.. code-block:: idris

docs/index.rst+1−1

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

64 effects/conclusions

65 effects/summary

66

67−.. _proofs::

67+.. _proofs:

68

69###############

70Theorem Proving

docs/tutorial/interp.rst+2−1

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

266program at the Idris interactive environment is:

267

268

269+.. _factrun:

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

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

270− :name: factrun

271+

271

272

272Aside: ``cast``

273Aside: ``cast``

273~~~~~~~~~~~~~~~

274~~~~~~~~~~~~~~~

docs/tutorial/modules.rst+4−2

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

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

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

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

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

13+``btree.idr``):

14

15.. code-block:: idris

16

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

32 toTree [] = Leaf

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

34

35+

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

36Then, 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:

37

38

38.. code-block:: idris

39.. code-block:: idris

39

40

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

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

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

46 print (btree.toList t)

47 print (btree.toList t)

47

48

49+

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

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

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

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

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

52The 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

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

87bytecode is regenerated if the source file changes.

88

89+.. _run1:

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

90.. 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:

221

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

223

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

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

225− application

225+

226

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

228

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

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

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

950

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

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

952− of the same type.

952+ value of the same type.

953

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

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

956 itself.

957