72f4386 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2151 from jfdm/doc/fixes

72f4386Jan de Muijnck-Hughes12 years ago

docs/tutorial/introduction.rst+10−10

compare with master

unifiedsplit

@@ -25,11 +25,12 @@ lists of a given length [1]_, ``Vect n a``, where ``a`` is the element

25type and ``n`` is the length of the list and can be an arbitrary term.

27When types can contain values, and where those values describe

28−properties (e.g. the length of a list) the type of a function can

28+properties, for example the length of a list, the type of a function

29−begin to describe its own properties. For example, concatenating two

29+can begin to describe its own properties. Take for example the

30+concatenatation of two lists. This operation has the property that the

30−lists has the property that the resulting list’s length is the sum of

31+resulting list's length is the sum of the lengths of the two input

31−the lengths of the two input lists. We can therefore give the

32+lists. We can therefore give the following type to the ``app``

32−following type to the ``app`` function, which concatenates vectors:

33+function, which concatenates vectors:

34.. code-block:: idris

35.. code-block:: idris

@@ -58,11 +59,10 @@ Example Code

58============

59============

60This tutorial includes some example code, which has been tested with

61This tutorial includes some example code, which has been tested with

61−Idris version . The files are available in the Idris

62+against Idris. These files are available with the Idris distribution,

62−distribution, and provided along side the tutorial source, so that you

63−can try them out easily, under ``tutorial/examples``. However, it is

63+so that you can try them out easily. They can be found under

64−strongly recommended that you can type them in yourself, rather than

64+``samples``. It is, however, strongly recommended that you type

65−simply loading and reading them.

65+them in yourself, rather than simply loading and reading them.

67.. [1]

68 Typically, and perhaps confusingly, referred to in the dependently

docs/tutorial/modules.rst+14−12

@@ -10,11 +10,11 @@ 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``):

15.. code-block:: idris

17− module btree

17+ module Btree

19 data BTree a = Leaf

20 | Node (BTree a) a (BTree a)

@@ -40,23 +40,24 @@ Then, this gives a main program (in a file

41 module Main

43− import btree

43+ import Btree

45 main : IO ()

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

47 print (btree.toList t)

50+

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

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

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

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

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

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

54−+ ``btree.BTree``

55++ ``Btree.BTree``

55−+ ``btree.Leaf``

56++ ``Btree.Leaf``

56−+ ``btree.Node``

57++ ``Btree.Node``

57−+ ``btree.insert``

58++ ``Btree.insert``

58−+ ``btree.toList``

59++ ``Btree.toList``

59−+ ``btree.toTree``

60++ ``Btree.toTree``

61If names are otherwise unambiguous, there is no need to give the fully

62If names are otherwise unambiguous, there is no need to give the fully

62qualified name. Names can be disambiguated either by giving an explicit

63qualified name. Names can be disambiguated either by giving an explicit

@@ -103,7 +104,7 @@ functions to be exported as ``abstract``, as we see below:

103

104

104.. code-block:: idris

105.. code-block:: idris

105

106

106− module btree

107+ module Btree

107

108

108 abstract data BTree a = Leaf

109 abstract data BTree a = Leaf

109 | Node (BTree a) a (BTree a)

110 | Node (BTree a) a (BTree a)

@@ -137,7 +138,8 @@ the ``public`` modifier on an ``import``. For example:

137

138

138 module A

139 module A

139

140

141+ import B

140− import B import public C

142+ import public C

141

143

142 public a : AType a = ...

144 public a : AType a = ...

143

145

@@ -154,7 +156,7 @@ wish to overload names within the same module:

154

156

155.. code-block:: idris

157.. code-block:: idris

156

158

157− module foo

159+ module Foo

158

160

159 namespace x

161 namespace x

160 test : Int -> Int

162 test : Int -> Int

docs/tutorial/starting.rst+9−13

@@ -10,12 +10,9 @@ Prerequisites

10Before installing Idris, you will need to make sure you have all

11of the necessary libraries and tools. You will need:

13−- A fairly recent Haskell platform. Version 2013.2.0.0 should be

14− sufficiently recent, though it is better to be completely up to

13+- A fairly recent Haskell platform. Version ``2013.2.0.0`` should be sufficiently recent, though it is better to be completely up to date.

15− date.

17−- The *GNU Multiple Precision Arithmetic Library* (GMP) is available

15+- The *GNU Multiple Precision Arithmetic Library* (GMP) is available from MacPorts/Homebrew and all major Linux distributions.

18− from MacPorts/Homebrew and all major Linux distributions.

20Downloading and Installing

17Downloading and Installing

21==========================

18==========================

@@ -33,7 +30,7 @@ development version you can find it, as well as build intructions, on

33GitHub at: https://github.com/idris-lang/Idris-dev.

30GitHub at: https://github.com/idris-lang/Idris-dev.

35To check that installation has succeeded, and to write your first

32To check that installation has succeeded, and to write your first

36−Idris program, create a file called “``hello.idr``” containing the

33+Idris program, create a file called ``hello.idr`` containing the

37following text:

34following text:

39.. code-block:: idris

36.. code-block:: idris

@@ -55,18 +52,17 @@ create an executable called ``hello``, which you can run:

55 $ ./hello

52 $ ./hello

56 Hello world

53 Hello world

58−Note that the ``$`` indicates the shell prompt! Should the Idris

55+Please note that the dollar sign ``$`` indicates the shell prompt!

59−executable not be found please ensure that you have added

56+Should the Idris executable not be found please ensure that you have

60−``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS X

57+added ``~/.cabal/bin`` to your ``$PATH`` environment variable. Mac OS

61−users may find they need to use ``~/Library/Haskell/bin``

58+X users may find they need to add ``~/Library/Haskell/bin``

62instead. Some useful options to the Idris command are:

59instead. Some useful options to the Idris command are:

64- ``-o prog`` to compile to an executable called ``prog``.

61- ``-o prog`` to compile to an executable called ``prog``.

66−- ``--check`` type check the file and its dependencies without

63+- ``--check`` type check the file and its dependencies without starting the interactive environment.

67− starting the interactive environment.

69−- ``--help`` display usage summary and command line options

65+- ``--help`` display usage summary and command line options.

71The Interactive Environment

67The Interactive Environment

72===========================

68===========================

docs/tutorial/typesfuns.rst+37−33

@@ -12,13 +12,13 @@ Idris defines several primitive types: ``Int``, ``Integer`` and

12manipulation, and ``Ptr`` which represents foreign pointers. There are

13also several data types declared in the library, including ``Bool``,

14with values ``True`` and ``False``. We can declare some constants with

15−these types. Enter the following into a file ``prims.idr`` and load it

15+these types. Enter the following into a file ``Prims.idr`` and load it

16into the Idris interactive environment by typing ``idris

17−prims.idr``:

17+Prims.idr``:

19.. code-block:: idris

21− module prims

21+ module Prims

23 x : Int

24 x = 42

@@ -33,17 +33,18 @@ prims.idr``:

33 quux = False

35An Idris file consists of an optional module declaration (here

36−``module prims``) followed by an optional list of imports (none here,

36+``module Prims``) followed by an optional list of imports and a

37+collection of declarations and definitions. In this example no imports

37−however Idris programs can consist of several modules, and the

38+have been specified. However Idris programs can consist of several

38−definitions in each module each have their own namespace, as we will

39+modules and the definitions in each module each have their own

39−discuss in Section :ref:`sect-namespaces`) and a collection of

40+namespace. This is discussed further in Section

40−declarations and definitions. The order of definitions is significant

41+:ref:`sect-namespaces`). When writing Idris programs both the order in

42+definitions are given and indentation are significant. Functions and

41−— functions and data types must be defined before use. Each definition

43+data types must be defined before use, incidently each definition must

42−must have a type declaration, for example see ``x : Int``, ``foo :

44+have a type declaration, for example see ``x : Int``, ``foo :

43−String``, from the above listing. Indentation is significant — a new

45+String``, from the above listing. New declarations must begin at the

44−declaration begins at the same level of indentation as the preceding

46+same level of indentation as the preceding declaration.

45−declaration. Alternatively, declarations may be terminated with a

47+Alternatively, a semicolon ``;`` can be used to terminate declarations.

46−semicolon.

48A library module ``prelude`` is automatically imported by every

49A library module ``prelude`` is automatically imported by every

49Idris program, including facilities for IO, arithmetic, data

50Idris program, including facilities for IO, arithmetic, data

@@ -63,7 +64,7 @@ All of the usual arithmetic and comparison operators are defined for

63the primitive types. They are overloaded using type classes, as we

64the primitive types. They are overloaded using type classes, as we

64will discuss in Section :ref:`sect-classes` and can be extended to

65will discuss in Section :ref:`sect-classes` and can be extended to

65work on user defined types. Boolean expressions can be tested with the

66work on user defined types. Boolean expressions can be tested with the

66−``if...then...else`` construct:

67+``if...then...else`` construct, for example:

68::

69::

@@ -73,9 +74,9 @@ work on user defined types. Boolean expressions can be tested with the

73Data Types

74Data Types

74==========

75==========

76−Data types are declared in a similar way to Haskell data types, with a

77+Data types are declared in a similar way and with similar syntax to

77−similar syntax. Natural numbers and lists, for example, can be

78+Haskell. Natural numbers and lists, for example, can be declared as

78−declared as follows:

79+follows:

80.. code-block:: idris

81.. code-block:: idris

@@ -193,11 +194,13 @@ does not need to be visible globally:

193Indentation is significant — functions in the ``where`` block must be

194Indentation is significant — functions in the ``where`` block must be

194indented further than the outer function.

195indented further than the outer function.

195

196

197+.. note:: Scope

198+

196−**Scope:** Any names which are visible in the outer scope are also

199+ Any names which are visible in the outer scope are also visible in

197−visible in the ``where`` clause (unless they have been redefined, such

200+ the ``where`` clause (unless they have been redefined, such as ``xs``

198−as ``xs`` here). A name which appears only in the type will be in scope

201+ here). A name which appears only in the type will be in scope in the

199−in the ``where`` clause if it is a *parameter* to one of the types,

202+ ``where`` clause if it is a *parameter* to one of the types, i.e. it

200−i.e. it is fixed across the entire structure.

203+ is fixed across the entire structure.

201

204

202As well as functions, ``where`` blocks can include local data

205As well as functions, ``where`` blocks can include local data

203declarations, such as the following where ``MyLT`` is not accessible

206declarations, such as the following where ``MyLT`` is not accessible

@@ -306,16 +309,17 @@ following:

306 $ idris vbroken.idr --check

309 $ idris vbroken.idr --check

307 vbroken.idr:9:23:When elaborating right hand side of Vect.++:

310 vbroken.idr:9:23:When elaborating right hand side of Vect.++:

308 When elaborating an application of constructor Vect.:::

311 When elaborating an application of constructor Vect.:::

309− Can't unify

312+ Can't unify

310− Vect (k + k) a

313+ Vect (k + k) a (Type of xs ++ xs)

311− with

314+ with

312− Vect (plus k m) a

315+ Vect (plus k m) a (Expected type)

313−

316+

314− Specifically:

317+ Specifically:

315− Can't unify

318+ Can't unify

316− plus k k

319+ plus k k

317− with

320+ with

318− plus k m

321+ plus k m

322+

319

323

320This error message suggests that there is a length mismatch between

324This error message suggests that there is a length mismatch between

321two vectors — we needed a vector of length ``k + m``, but provided a

325two vectors — we needed a vector of length ``k + m``, but provided a

docs/tutorial/views.rst+2−2

@@ -83,8 +83,8 @@ rule:

83The value of the result of ``parity k`` affects the form of ``k``,

84because the result of ``parity k`` depends on ``k``. So, as well as

85the patterns for the result of the intermediate computation (``Even``

86−and ``odd``) right of the ``\mid``, we also write how the results

86+and ``odd``) right of the ``|``, we also write how the results

87−affect the other patterns left of the :math:`\mid`. Note that there is

87+affect the other patterns left of the ``|``. Note that there is

88a function in the patterns (``+``) and repeated occurrences of

89``j``—this is allowed because another argument has determined the form

90of these patterns.