ffd720a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #4408 from OlingCat/master

Fix some typos and normalize the use of punctuations.

commitffd720aeec6254fda134487817a0db5a86435b24 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateTue 3 Apr 2018, 10:10 (9 years ago) parent4c5c430 ba99edd

11 files changed+137−131

compare with master

unifiedsplit

docs/faq/faq.rst+14−5 docs/st/composing.rst+16−16 docs/tutorial/interactive.rst+4−5 docs/tutorial/interfaces.rst+6−7 docs/tutorial/interp.rst+2−2 docs/tutorial/miscellany.rst+19−19 docs/tutorial/modules.rst+8−11 docs/tutorial/packages.rst+39−29 docs/tutorial/syntax.rst+4−4 docs/tutorial/theorems.rst+3−3 docs/tutorial/typesfuns.rst+22−30

docs/faq/faq.rst+14−5

@@ -173,8 +173,10 @@ function back to itself. On such a path, there must be at least one

173173argument which converges to a base case.

174174

175175- Mutually recursive functions are supported

176+

176177- However, all functions on the path must be fully applied. In particular,

177178 higher order applications are not supported

179+

178180- Idris identifies arguments which converge to a base case by looking for

179181 recursive calls to syntactically smaller arguments of inputs. e.g.

180182 ``k`` is syntactically smaller than ``S (S k)`` because ``k`` is a

@@ -233,14 +235,17 @@ where the install directory is unknown at build time. When passing this

233235flag, the IDRIS_LIB_DIR environment variable needs to be set to the path

234236where the Idris libs reside relative to the idris executable. The

235237IDRIS_TOOLCHAIN_DIR environment variable is optional, if that is set,

236−Idris will use that path to find the C compiler.

238+Idris will use that path to find the C compiler. For example:

237239

238−Example::

240+::

239241

240− IDRIS_LIB_DIR="./libs" IDRIS_TOOLCHAIN_DIR="./mingw/bin" CABALFLAGS="-fffi -ffreestanding -frelease" make

242+ IDRIS_LIB_DIR="./libs" \

243+ IDRIS_TOOLCHAIN_DIR="./mingw/bin" \

244+ CABALFLAGS="-fffi -ffreestanding -frelease" \

245+ make

241246

242247

243−What does the name ‘Idris’ mean?

248+What does the name “Idris” mean?

244249================================

245250

246251British people of a certain age may be familiar with this

@@ -256,16 +261,20 @@ There are several reasons why we should not support Unicode operators:

256261- It's hard to type (this is important if you're using someone else's code, for

257262 example). Various editors have their own input methods, but you have to know

258263 what they are.

264+

259265- Not every piece of software easily supports it. Rendering issues have been

260266 noted on some mobile email clients, terminal-based IRC clients, web browsers,

261267 etc. There are ways to resolve these rendering issues but they provide a

262268 barrier to entry to using Idris.

269+

263270- Even if we leave it out of the standard library (which we will in any case!)

264271 as soon as people start using it in their library code, others have to deal

265272 with it.

273+

266274- Too many characters look too similar. We had enough trouble with confusion

267275 between 0 and O without worrying about all the different kinds of colons and

268276 brackets.

277+

269278- There seems to be a tendency to go over the top with use of Unicode. For

270279 example, using sharp and flat for delay and force (or is it the other way

271280 around?) in Agda seems gratuitous. We don't want to encourage this sort of

@@ -280,7 +289,7 @@ This seems like an instance of `Wadler's

280289Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.

281290

282291This answer is based on Edwin Brady's response in the following

283−`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`__.

292+`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`_.

284293

285294Where can I find the community standards for the Idris community?

286295==================================================================

docs/st/composing.rst+16−16

@@ -1,7 +1,7 @@

11.. _composing:

33************************

4−Composing State Machines

4+Composing State Machines

55************************

77In the previous section, we defined a ``DataStore`` interface and used it

@@ -28,7 +28,7 @@ there was a login failure in a state.

2828

2929Furthermore, we may have *hierarchies* of state machines, in that one

3030state machine could be implemented by composing several others. For

31−example, we can have a state machine representing the state of a

31+example, we can have a state machine representing the state of a

3232graphics system, and use this to implement a *higher level* graphics API

3333such as turtle graphics, which uses the graphics system plus some additional

3434state for the turtle.

@@ -50,7 +50,7 @@ count to zero, a session might run as follows:

5050 *LoginCount> :exec main

5151 Enter password: Mornington Crescent

5252 Secret is: "Secret Data"

53− Enter password: Dollis Hill

53+ Enter password: Dollis Hill

5454 Failure

5555 Number of failures: 1

5656 Enter password: Mornington Crescent

@@ -63,7 +63,7 @@ count to zero, a session might run as follows:

6363We'll start by adding a state resource to ``getData`` to keep track of the

6464number of failures:

6565

66−.. code-block:: idrs

66+.. code-block:: idris

6767

6868 getData : (ConsoleIO m, DataStore m) =>

6969 (failcount : Var) -> ST m () [failcount ::: State Integer]

@@ -116,7 +116,7 @@ match:

116116 Required result states here are: st2_fn

117117

118118In other words, ``connect`` requires that there are *no* resources on

119−entry, but we have *one*, the failure count!

119+entry, but we have *one*, the failure count!

120120This shouldn't be a problem, though: the required resources are a *subset* of

121121the resources we have, after all, and the additional resources (here, the

122122failure count) are not relevant to ``connect``. What we need, therefore,

@@ -214,7 +214,7 @@ ordering of resources is allowed to change, although resources which

214214appear in ``old`` can't appear in the ``sub`` list more than once (you will

215215get a type error if you try this).

216216

217−The function ``updateWith`` takes the *output* resources of the

217+The function ``updateWith`` takes the *output* resources of the

218218called function, and updates them in the current resource list. It makes

219219an effort to preserve ordering as far as possible, although this isn't

220220always possible if the called function does some complicated resource

@@ -338,7 +338,7 @@ representing a surface on which we'll draw lines and rectangles:

338338

339339.. code-block:: idris

340340

341− interface Draw (m : Type -> Type) where

341+ interface Draw (m : Type -> Type) where

342342 Surface : Type

343343

344344We'll need to be able to create a new ``Surface`` by opening a window:

@@ -369,7 +369,7 @@ succeeds (that is, returns a result of the form ``Just val``.

369369 an operation returns ``Just ty``, there's also ``addIfRight``:

370370

371371 .. code-block:: idris

372−

372+

373373 addIfJust : Type -> Action (Maybe Var)

374374 addIfRight : Type -> Action (Either a Var)

375375

@@ -378,10 +378,10 @@ succeeds (that is, returns a result of the form ``Just val``.

378378 of an operation:

379379

380380 .. code-block:: idris

381−

381+

382382 Add : (ty -> Resources) -> Action ty

383−

384− Using this, you can create your own actions to add resources

383+

384+ Using this, you can create your own actions to add resources

385385 based on the result of an operation, if required. For example,

386386 ``addIfJust`` is implemented as follows:

387387

@@ -479,7 +479,7 @@ For example, assuming we have a surface ``win`` to draw onto, we can write a

479479

480480The ``flip win`` at the end is necessary because the drawing primitives

481481are double buffered, to prevent flicker. We draw onto one buffer, off-screen,

482−and display the other. When we call ``flip``, it displays the off-screen

482+and display the other. When we call ``flip``, it displays the off-screen

483483buffer, and creates a new off-screen buffer for drawing the next frame.

484484

485485To include this in a program, we'll write a main loop which renders our

@@ -496,7 +496,7 @@ application:

496496

497497Finally, we can create a main program which initialises a window, if

498498possible, then runs the main loop:

499−

499+

500500.. code-block:: idris

501501

502502 drawMain : (ConsoleIO m, Draw m) => ST m () []

@@ -593,7 +593,7 @@ is implemented using the following type, defined by ``Control.ST``:

593593

594594.. code-block:: idris

595595

596− data Composite : List Type -> Type

596+ data Composite : List Type -> Type

597597

598598If we have a composite resource, we can split it into its constituent

599599resources, and create new variables for each of those resources, using

@@ -604,7 +604,7 @@ the *split* function. For example:

604604 splitComp : (comp : Var) -> ST m () [comp ::: Composite [State Int, State String]]

605605 splitComp comp = do [int, str] <- split comp

606606 ?whatNow

607−

607+

608608The call ``split comp`` extracts the ``State Int`` and ``State String`` from

609609the composite resource ``comp``, and stores them in the variables ``int``

610610and ``str`` respectively. If we check the type of ``whatNow``, we'll see

@@ -713,7 +713,7 @@ A ``Line`` is defined as a start location, and end location, and a colour:

713713 Line : Type

714714 Line = ((Int, Int), (Int, Int), Col)

715715

716−To implement ``start``, which creates a new ``Turtle`` (or returns ``Nothing``

716+To implement ``start``, which creates a new ``Turtle`` (or returns ``Nothing``

717717if this is impossible), we begin by initialising the drawing surface then

718718all of the components of the state. Finally, we combine all of these

719719into a composite resource for the turtle:

docs/tutorial/interactive.rst+4−5

@@ -23,7 +23,6 @@ editor, and specifically how to do so in `Vim

2323for `Emacs <https://github.com/idris-hackers/idris-mode>`_ is also

2424available.

2525

26−

2726Editing at the REPL

2827===================

2928

@@ -64,9 +63,9 @@ Editing Commands

6463:addclause

6564----------

6665

67−The ``:addclause n f`` command (abbreviated ``:ac n f``) creates a

66+The ``:addclause n f`` command, abbreviated ``:ac n f``, creates a

6867template definition for the function named ``f`` declared on line

69−``n``. For example, if the code beginning on line 94 contains:

68+``n``. For example, if the code beginning on line 94 contains:

7069

7170.. code-block:: idris

7271

@@ -129,7 +128,7 @@ ys`` would lead to a unification error.

129128

130129The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the

131130clauses which are required to make the function ``f`` on line ``n``

132−cover all inputs. For example, if the code beginning on line 94 is

131+cover all inputs. For example, if the code beginning on line 94 is:

133132

134133.. code-block:: idris

135134

@@ -143,7 +142,7 @@ then ``:am 96 vzipWith`` gives:

143142

144143 vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2

145144

146−That is, it notices that there are no cases for non-empty vectors,

145+That is, it notices that there are no cases for empty vectors,

147146generates the required clauses, and eliminates the clauses which would

148147lead to unification errors.

149148

docs/tutorial/interfaces.rst+6−7

@@ -11,8 +11,8 @@ data types. For example, we would like arithmetic operators to work on

1111to display different types in a uniform way.

1212

1313To achieve this, we use *interfaces*, which are similar to type classes in

14−Haskell or traits in Rust. To define an interface, we provide a collection of

15−overloadable functions. A simple example is the ``Show``

14+Haskell or traits in Rust. To define an interface, we provide a collection of

15+overloadable functions. A simple example is the ``Show``

1616interface, which is defined in the prelude and provides an interface for

1717converting values to ``String``:

1818

@@ -31,8 +31,7 @@ This generates a function of the following type (which we call a

3131We can read this as: “under the constraint that ``a`` has an implementation

3232of ``Show``, take an input ``a`` and return a ``String``.” An implementation

3333of an interface is defined by giving definitions of the methods of the interface.

34−For example, the

35−``Show`` implementation for ``Nat`` could be defined as:

34+For example, the ``Show`` implementation for ``Nat`` could be defined as:

3635

3736.. code-block:: idris

3837

@@ -49,7 +48,7 @@ Only one implementation of an interface can be given for a type — implementati

4948not overlap. Implementation declarations can themselves have constraints.

5049To help with resolution, the arguments of an implementation must be

5150constructors (either data or type constructors) or variables

52−(i.e. you cannot give an implementation for a function). For

51+(i.e. you cannot give an implementation for a function). For

5352example, to define a ``Show`` implementation for vectors, we need to know

5453that there is a ``Show`` implementation for the element type, because we are

5554going to use it to convert each element to a ``String``:

@@ -534,7 +533,7 @@ Named Implementations

534533

535534It can be desirable to have multiple implementations of an interface for the

536535same type, for example to provide alternative methods for sorting or printing

537−values. To achieve this, implementations can be *named* as follows:

536+values. To achieve this, implementations can be *named* as follows:

538537

539538.. code-block:: idris

540539

@@ -574,7 +573,7 @@ the prelude defines the following ``Semigroup`` interface:

574573 interface Semigroup ty where

575574 (<+>) : ty -> ty -> ty

576575

577−Then it defines ``Monoid``, which extends ``Semigroup`` with a "neutral"

576+Then it defines ``Monoid``, which extends ``Semigroup`` with a “neutral”

578577value:

579578

580579.. code-block:: idris

docs/tutorial/interp.rst+2−2

@@ -106,7 +106,7 @@ the ``Var`` constructor:

106106

107107 Var : HasType i G t -> Expr G t

108108

109−So, in an expression ``\x,\y. x y``, the variable ``x`` would have a

109+So, in an expression ``\x. \y. x y``, the variable ``x`` would have a

110110de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,

111111represented as ``Stop``. We find these by counting the number of

112112lambdas between the definition and the use.

@@ -194,7 +194,7 @@ each constructor, we translate it into the corresponding Idris value:

194194 interp env (If x t e) = if interp env x then interp env t

195195 else interp env e

196196

197−Let us look at each case in turn. To translate a variable, we simply look it

197+Let us look at each case in turn. To translate a variable, we simply look it

198198up in the environment:

199199

200200.. code-block:: idris

docs/tutorial/miscellany.rst+19−19

@@ -8,7 +8,7 @@ In this section we discuss a variety of additional features:

99+ auto, implicit, and default arguments;

1010+ literate programming;

11−+ interfacing with external libraries through the foreign function

11++ interfacing with external libraries through the foreign function;

1212+ interface;

1313+ type providers;

1414+ code generation; and

@@ -23,7 +23,7 @@ omitted when they can be inferred by the type checker, e.g.

2323.. code-block:: idris

2424

2525 index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

26−

26+

2727Auto implicit arguments

2828------------------------

2929

@@ -69,17 +69,17 @@ In the case that a proof is not found, it can be provided explicitly as normal:

6969.. code-block:: idris

7070

7171 head xs {p = ?headProof}

72−

72+

7373Default implicit arguments

7474---------------------------

7575

76−Besides having Idris automatically find a value of a given type, sometimes we

76+Besides having Idris automatically find a value of a given type, sometimes we

7777want to have an implicit argument with a specific default value. In Idris, we can

7878do this using the ``default`` annotation. While this is primarily intended to assist

79−in automatically constructing a proof where auto fails, or finds an unhelpful value,

80−it might be easier to first consider a simpler case, not involving proofs.

79+in automatically constructing a proof where auto fails, or finds an unhelpful value,

80+it might be easier to first consider a simpler case, not involving proofs.

8181

82−If we want to compute the n'th fibonacci number (and defining the 0th fibonacci

82+If we want to compute the n'th fibonacci number (and defining the 0th fibonacci

8383number as 0), we could write:

8484

8585.. code-block:: idris

@@ -89,8 +89,8 @@ number as 0), we could write:

8989 fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n

9090

9191After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,

92−and will return the 5th fibonacci number. Note that while this works, this is not the

93−intended use of the ``default`` annotation. It is included here for illustrative purposes

92+and will return the 5th fibonacci number. Note that while this works, this is not the

93+intended use of the ``default`` annotation. It is included here for illustrative purposes

9494only. Usually, ``default`` is used to provide things like a custom proof search script.

9595

9696

@@ -329,13 +329,13 @@ are available in an external collection [1]_.

329329C Target

330330========

331331

332−The default target of Idris is C. Compiling via :

332+The default target of Idris is C. Compiling via:

333333

334334::

335335

336336 $ idris hello.idr -o hello

337337

338−is equivalent to :

338+is equivalent to:

339339

340340::

341341

@@ -344,14 +344,14 @@ is equivalent to :

344344When the command above is used, a temporary C source is generated, which

345345is then compiled into an executable named ``hello``.

346346

347−In order to view the generated C code, compile via :

347+In order to view the generated C code, compile via:

348348

349349::

350350

351351 $ idris hello.idr -S -o hello.c

352352

353353To turn optimisations on, use the ``%flag C`` pragma within the code, as

354−is shown below :

354+is shown below:

355355

356356.. code-block:: idris

357357

@@ -368,7 +368,7 @@ is shown below :

368368

369369To compile the generated C with debugging information e.g. to use

370370``gdb`` to debug segmentation faults in Idris programs, use the

371−``%flag C`` pragma to include debugging symbols, as is shown below :

371+``%flag C`` pragma to include debugging symbols, as is shown below:

372372

373373.. code-block:: idris

374374

@@ -503,13 +503,13 @@ And for use in the browser:

503503

504504The given files will be added to the top of the generated code.

505505For library packages you can also use the ipkg objs option to include the

506−js file in the installation, and use

506+js file in the installation, and use:

507507

508508.. code-block:: idris

509509

510510 %include Node "package/external.js"

511511

512−This javascript and node backends idris will also lookup for the file on

512+The *JavaScript* and *NodeJS* backends of Idris will also lookup for the file

513513on that location.

514514

515515Including *NodeJS* modules

@@ -552,7 +552,7 @@ types themselves have types. For example:

552552 *universe> :t Vect

553553 Vect : Nat -> Type -> Type

554554

555−But what about the type of ``Type``? If we ask Idris it reports

555+But what about the type of ``Type``? If we ask Idris it reports:

556556

557557::

558558

@@ -560,8 +560,8 @@ But what about the type of ``Type``? If we ask Idris it reports

560560 Type : Type 1

561561

562562If ``Type`` were its own type, it would lead to an inconsistency due to

563−`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_ , so internally there is a

564−*hierarchy* of types (or *universes*):

563+`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,

564+so internally there is a *hierarchy* of types (or *universes*):

565565

566566.. code-block:: idris

567567

docs/tutorial/modules.rst+8−11

@@ -53,8 +53,7 @@ Then, this gives a main program (in a file

5353 print (Btree.toList t)

5454

5555The same names can be defined in multiple modules: names are *qualified* with

56−the name of the module. The names defined in the ``Btree`` module are, in

57−full:

56+the name of the module. The names defined in the ``Btree`` module are, in full:

5857

5958+ ``Btree.BTree``

6059+ ``Btree.Leaf``

@@ -74,7 +73,7 @@ directories. For example, ``import foo.bar`` would import the file

7473``foo/bar.idr``, which would conventionally have the module declaration

7574``module foo.bar``. The only requirement for module names is that the

7675main module, with the ``main`` function, must be called

77−``Main``—although its filename need not be ``Main.idr``.

76+``Main`` — although its filename need not be ``Main.idr``.

7877

7978Export Modifiers

8079================

@@ -82,18 +81,16 @@ Export Modifiers

8281Idris allows for fine-grained control over the visibility of a

8382module's contents. By default, all names defined in a module are kept

8483private. This aides in specification of a minimal interface and for

85−internal details to be left hidden. Idris allows for functions,

84+internal details to be left hidden. Idris allows for functions,

8685types, and interfaces to be marked as: ``private``, ``export``, or

87−``public export``. Their general meaning is as follows:

86+``public export``. Their general meaning is as follows:

8887

89−- ``private`` meaning that it's not exported at all. This is the

90− default.

88+- ``private`` meaning that it's not exported at all. This is the default.

9189

9290- ``export`` meaning that its top level type is exported.

9391

9492- ``public export`` meaning that the entire definition is exported.

9593

96−

9794A further restriction in modifying the visibility is that definitions

9895must not refer to anything within a lower level of visibility. For

9996example, ``public export`` definitions cannot use private names, and

@@ -129,10 +126,9 @@ Meaning for Data Types

129126

130127For data types, the meanings are:

131128

132−- ``export`` the type constructor is exported

129+- ``export`` the type constructor is exported

133130

134−- ``public export`` the type constructor and data constructors are

135− exported

131+- ``public export`` the type constructor and data constructors are exported

136132

137133

138134Meaning for Interfaces

@@ -141,6 +137,7 @@ Meaning for Interfaces

141137For interfaces, the meanings are:

142138

143139- ``export`` the interface name is exported

140+

144141- ``public export`` the interface name, method names and default

145142 definitions are exported

146143

docs/tutorial/packages.rst+39−29

@@ -1,26 +1,31 @@

1+.. _sect-packages:

13********

24Packages

35********

5−

6−Idris includes a simple build system for building packages and executables from a named package description file.

7−These files can be used with the Idris compiler to manage the development process .

7+Idris includes a simple build system for building packages and executables

8+from a named package description file. These files can be used with the

9+Idris compiler to manage the development process .

810

911Package Descriptions

1012====================

1113

1214A package description includes the following:

1315

14−+ A header, consisting of the keyword package followed by the package

16++ A header, consisting of the keyword ``package`` followed by a package

1517 name. Package names can be any valid Idris identifier. The iPKG

1618 format also takes a quoted version that accepts any valid filename.

17−+ Fields describing package contents, ``<field> = <value>``

19+

20++ Fields describing package contents, ``<field> = <value>``.

1821

1922At least one field must be the modules field, where the value is a

20−comma separated list of modules. For example, given an idris package

23+comma separated list of modules. For example, given an idris package

2124``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,

2225``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding

23−package file would be::

26+package file would be:

27+

28+::

2429

2530 package maths

2631

@@ -38,7 +43,6 @@ of the main Idris repository, and in `third-party libraries

3843Using Package files

3944===================

4045

41−

4246Idris itself is aware about packages, and special commands are

4347available to help with, for example, building packages, installing

4448packages, and cleaning packages. For instance, given the ``maths``

@@ -54,7 +58,9 @@ package from earlier we can use Idris as follows:

5458

5559Once the maths package has been installed, the command line option

5660``--package maths`` makes it accessible (abbreviated to ``-p maths``).

57−For example::

61+For example:

62+

63+::

5864

5965 idris -p maths Main.idr

6066

@@ -66,20 +72,18 @@ The integrated build system includes a simple testing framework.

6672This framework collects functions listed in the ``ipkg`` file under ``tests``.

6773All test functions must return ``IO ()``.

6874

69−

7075When you enter ``idris --testpkg yourmodule.ipkg``,

7176the build system creates a temporary file in a fresh environment on your machine

7277by listing the ``tests`` functions under a single ``main`` function.

7378It compiles this temporary file to an executable and then executes it.

7479

75−

7680The tests themselves are responsible for reporting their success or failure.

7781Test functions commonly use ``putStrLn`` to report test results.

7882The test framework does not impose any standards for reporting and consequently

7983does not aggregate test results.

8084

81−

82−For example, lets take the following list of functions that are defined in a module called ``NumOps`` for a sample package ``maths``.

85+For example, lets take the following list of functions that are defined in a

86+module called ``NumOps`` for a sample package ``maths``:

8387

8488.. name: Math/NumOps.idr

8589.. code-block:: idris

@@ -94,7 +98,8 @@ For example, lets take the following list of functions that are defined in a mod

9498 triple : Num a => a -> a

9599 triple a = a + double a

96100

97−A simple test module, with a qualified name of ``Test.NumOps`` can be declared as

101+

102+A simple test module, with a qualified name of ``Test.NumOps`` can be declared as:

98103

99104.. name: Math/TestOps.idr

100105.. code-block:: idris

@@ -122,8 +127,11 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a

122127 testTriple = assertNotEq (triple 2) 5

123128

124129

125−The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing, and failing, equality tests.

126−The actual tests are ``testDouble`` and ``testTriple``, and are declared in the ``maths.ipkg`` file as follows::

130+The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing,

131+and failing, equality tests. The actual tests are ``testDouble`` and ``testTriple``,

132+and are declared in the ``maths.ipkg`` file as follows:

133+

134+::

127135

128136 package maths

129137

@@ -134,7 +142,9 @@ The actual tests are ``testDouble`` and ``testTriple``, and are declared in the

134142 , Test.NumOps.testTriple

135143

136144

137−The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::

145+The testing framework can then be invoked using ``idris --testpkg maths.ipkg``:

146+

147+::

138148

139149 > idris --testpkg maths.ipkg

140150 Type checking ./Maths/NumOps.idr

@@ -146,25 +156,25 @@ The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::

146156Note how both tests have reported success by printing ``Test Passed``

147157as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.

148158

149−Package Dependencies Using Atom

159+Package Dependencies Using Atom

150160===============================

151161

152−If you are using the Atom editor and have a dependency on another package,

153−corresponding to for instance ``import Lightyear`` or ``import Pruviloj``,

154−you need to let Atom know that it should be loaded. The easiest way to

155−accomplish that is with a .ipkg file. The general contents of an ipkg file

156−will be described in the next section of the tutorial, but for now here is

157−a simple recipe for this trivial case.

162+If you are using the Atom editor and have a dependency on another package,

163+corresponding to for instance ``import Lightyear`` or ``import Pruviloj``,

164+you need to let Atom know that it should be loaded. The easiest way to

165+accomplish that is with a .ipkg file. The general contents of an ipkg file

166+will be described in the next section of the tutorial, but for now here is

167+a simple recipe for this trivial case:

158168

159−- Create a folder myProject.

169+- Create a folder myProject.

160170

161−- Add a file myProject.ipkg containing just a couple of lines:

171+- Add a file myProject.ipkg containing just a couple of lines:

162172

163−``package myProject``

173+``package myProject``

164174

165−``pkgs = pruviloj, lightyear``

175+``pkgs = pruviloj, lightyear``

166176

167−- In Atom, use the File menu to Open Folder myProject.

177+- In Atom, use the File menu to Open Folder myProject.

168178

169179More information

170180================

docs/tutorial/syntax.rst+4−4

@@ -34,7 +34,7 @@ rule, and the right hand side describes its expansion. The syntax rule

3434itself consists of:

3535

3636- **Keywords** — here, ``if``, ``then`` and ``else``, which must be

37− valid identifiers

37+ valid identifiers.

3838

3939- **Non-terminals** — included in square brackets, ``[test]``, ``[t]``

4040 and ``[e]`` here, which stand for arbitrary expressions. To avoid

@@ -44,9 +44,9 @@ itself consists of:

4444- **Names** — included in braces, which stand for names which may be

4545 bound on the right hand side.

4646

47−- **Symbols** — included in quotations marks, e.g. ``:=``. This can

47+- **Symbols** — included in quotations marks, e.g. ``":="``. This can

4848 also be used to include reserved words in syntax rules, such as

49− ``let`` or ``in``.

49+ ``"let"`` or ``"in"``.

5050

5151The limitations on the form of a syntax rule are that it must include

5252at least one symbol or keyword, and there must be no repeated

@@ -63,7 +63,7 @@ recursive. The following syntax extensions would therefore be valid:

6363 syntax select [x] from [t] "where" [w] = SelectWhere x t w;

6464 syntax select [x] from [t] = Select x t;

6565

66−Syntax macros can be further restricted to apply only in patterns (i.e.,

66+Syntax macros can be further restricted to apply only in patterns (i.e.

6767only on the left hand side of a pattern match clause) or only in terms

6868(i.e. everywhere but the left hand side of a pattern match clause) by

6969being marked as ``pattern`` or ``term`` syntax rules. For example, we

docs/tutorial/theorems.rst+3−3

@@ -115,8 +115,8 @@ We can do the same for the reduction behaviour of plus on successors:

115115

116116Even for trivial theorems like these, the proofs are a little tricky to

117117construct in one go. When things get even slightly more complicated, it

118−becomes too much to think about to construct proofs in this ‘batch

119−mode’.

118+becomes too much to think about to construct proofs in this “batch

119+mode”.

120120

121121Idris provides interactive editing capabilities, which can help with

122122building proofs. For more details on building proofs interactively in

@@ -383,7 +383,7 @@ will always be smaller than ``(x :: xs)``:

383383 = qsort (filter (< x) xs) ++

384384 (x :: qsort (filter (>= x) xs))

385385

386−The function ``assert_smaller``, defined in the Prelude, is intended to

386+The function ``assert_smaller``, defined in the prelude, is intended to

387387address this problem:

388388

389389.. code-block:: idris

docs/tutorial/typesfuns.rst+22−30

@@ -13,8 +13,7 @@ manipulation, and ``Ptr`` which represents foreign pointers. There are

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

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

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

16−into the Idris interactive environment by typing ``idris

17−Prims.idr``:

16+into the Idris interactive environment by typing ``idris Prims.idr``:

1817

1918.. code-block:: idris

2019

@@ -38,7 +37,7 @@ collection of declarations and definitions. In this example no imports

3837have been specified. However Idris programs can consist of several

3938modules and the definitions in each module each have their own

4039namespace. This is discussed further in Section

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

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

4241definitions are given and indentation are significant. Functions and

4342data types must be defined before use, incidentally each definition must

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

@@ -343,7 +342,7 @@ Vectors

343342

344343A standard example of a dependent data type is the type of “lists with

345344length”, conventionally called vectors in the dependent type

346−literature. They are available as part of the Idris library, by

345+literature. They are available as part of the Idris library, by

347346importing ``Data.Vect``, or we can declare them as follows:

348347

349348.. code-block:: idris

@@ -521,8 +520,8 @@ help document a function by making the purpose of an argument more

521520clear.

522521

523522Furthermore, ``{}`` can be used to pattern match on the left hand side, i.e.

524−``{var = pat}`` gets an implicit variable and attempts to pattern match on "pat";

525−For example :

523+``{var = pat}`` gets an implicit variable and attempts to pattern match on “pat”;

524+For example:

526525

527526.. code-block:: idris

528527

@@ -559,7 +558,6 @@ vector. For example:

559558 inVect : IsElem 5 Main.testVec

560559 inVect = There (There Here)

561560

562−

563561.. important:: Implicit Arguments and Scope

564562

565563 Within the type signature the typechecker will treat all variables

@@ -569,7 +567,6 @@ vector. For example:

569567 ``testVec``. In the example above, we have assumed that the code

570568 lives within the ``Main`` module.

571569

572−

573570If the same implicit arguments are being used a lot, it can make a

574571definition difficult to read. To avoid this problem, a ``using`` block

575572gives the types and ordering of any implicit arguments which can

@@ -582,15 +579,13 @@ appear within the block:

582579 Here : IsElem x (x :: xs)

583580 There : IsElem x xs -> IsElem x (y :: xs)

584581

585−

586−

587582Note: Declaration Order and ``mutual`` blocks

588583~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

589584

590585In general, functions and data types must be defined before use, since

591586dependent types allow functions to appear as part of types, and type

592587checking can rely on how particular functions are defined (though this

593−is only true of total functions; see Section :ref:`sect-totality`)).

588+is only true of total functions; see Section :ref:`sect-totality`).

594589However, this restriction can be relaxed by using a ``mutual`` block,

595590which allows data types and functions to be defined simultaneously:

596591

@@ -673,7 +668,7 @@ Note that several of these return ``Either``, since they may fail.

673668I/O programs will typically need to sequence actions, feeding the

674669output of one computation into the input of the next. ``IO`` is an

675670abstract type, however, so we can’t access the result of a computation

676−directly. Instead, we sequence operations with ``do`` notation:

671+directly. Instead, we sequence operations with ``do`` notation:

677672

678673.. code-block:: idris

679674

@@ -713,7 +708,7 @@ not always the best approach. Consider the following function:

713708

714709This function uses one of the ``t`` or ``e`` arguments, but not both

715710(in fact, this is used to implement the ``if...then...else`` construct

716−as we will see later. We would prefer if *only* the argument which was

711+as we will see later). We would prefer if *only* the argument which was

717712used was evaluated. To achieve this, Idris provides a ``Lazy``

718713data type, which allows evaluation to be suspended:

719714

@@ -797,7 +792,7 @@ infinite loop and cause a stack overflow.

797792To fix this we must add explicit ``Inf`` declarations to the constructor

798793parameter types, since codata will not add it to constructor parameters of a

799794**different** type from the one being defined. For example, the following

800−outputs "1".

795+outputs ``1``.

801796

802797.. code-block:: idris

803798

@@ -902,7 +897,7 @@ For more details of the functions available on ``List`` and

902897

903898- ``libs/base/Data/VectType.idr``

904899

905−Functions include filtering, appending, reversing, and so on.

900+Functions include filtering, appending, reversing, and so on.

906901

907902Aside: Anonymous functions and operator sections

908903~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

@@ -999,7 +994,7 @@ Dependent Pairs

999994---------------

1000995

1001996Dependent pairs allow the type of the second element of a pair to depend

1002−on the value of the first element.

997+on the value of the first element:

1003998

1004999.. code-block:: idris

10051000

@@ -1009,7 +1004,7 @@ on the value of the first element.

10091004Again, there is syntactic sugar for this. ``(a : A ** P)`` is the type

10101005of a pair of A and P, where the name ``a`` can occur inside ``P``.

10111006``( a ** p )`` constructs a value of this type. For example, we can

1012−pair a number with a ``Vect`` of a particular length.

1007+pair a number with a ``Vect`` of a particular length:

10131008

10141009.. code-block:: idris

10151010

@@ -1017,7 +1012,7 @@ pair a number with a ``Vect`` of a particular length.

10171012 vec = (2 ** [3, 4])

10181013

10191014If you like, you can write it out the long way, the two are precisely

1020−equivalent.

1015+equivalent:

10211016

10221017.. code-block:: idris

10231018

@@ -1070,7 +1065,7 @@ intermediate values:

10701065

10711066We will see more on ``with`` notation later.

10721067

1073−Dependent pairs are sometimes referred to as “sigma types”.

1068+Dependent pairs are sometimes referred to as “Sigma types”.

10741069

10751070Records

10761071-------

@@ -1080,7 +1075,7 @@ Records

10801075automatically generating field access and update functions. Unlike

10811076the syntax used for data structures, records in Idris follow a

10821077different syntax to that seen with Haskell. For example, we can

1083−represent a person's name and age in a record:

1078+represent a person’s name and age in a record:

10841079

10851080.. code-block:: idris

10861081

@@ -1092,12 +1087,11 @@ represent a person's name and age in a record:

10921087 fred : Person

10931088 fred = MkPerson "Fred" "Joe" "Bloggs" 30

10941089

1095−

10961090The constructor name is provided using the ``constructor`` keyword,

10971091and the *fields* are then given which are in an indented block

10981092following the `where` keyword (here, ``firstName``, ``middleName``,

10991093``lastName``, and ``age``). You can declare multiple fields on a

1100−single line, provided that they have the same type. The field names

1094+single line, provided that they have the same type. The field names

11011095can be used to access the field values:

11021096

11031097::

@@ -1171,7 +1165,7 @@ syntax:

11711165 record { a->b->c = val } x

11721166

11731167This returns a new record, with the field accessed by the path

1174−``a->b->c`` set to ``val``. The syntax is first class, i.e. ``record {

1168+``a->b->c`` set to ``val``. The syntax is first class, i.e. ``record {

11751169a->b->c = val }`` itself has a function type. Symmetrically, the field

11761170can also be accessed with the following syntax:

11771171

@@ -1196,12 +1190,10 @@ name. For example, a pair type could be defined as follows:

11961190 fst : a

11971191 snd : b

11981192

1199−

12001193Using the ``class`` record from earlier, the size of the class can be

12011194restricted using a ``Vect`` and the size included in the type by parameterising

12021195the record with the size. For example:

12031196

1204−

12051197.. code-block:: idris

12061198

12071199 record SizedClass (size : Nat) where

@@ -1214,7 +1206,7 @@ function from earlier, since that would change the size of the class. A

12141206function to add a student must now specify in the type that the

12151207size of the class has been increased by one. As the size is specified

12161208using natural numbers, the new value can be incremented using the

1217−``S`` constructor.

1209+``S`` constructor:

12181210

12191211.. code-block:: idris

12201212

@@ -1327,7 +1319,7 @@ matching ``let`` and lambda bindings. It will *only* work if:

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

13281320 value of the same type.

13291321

1330−- The type of the result is "known". i.e. the type of the expression

1322+- The type of the result is “known”. i.e. the type of the expression

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

13321324 itself.

13331325

@@ -1337,7 +1329,7 @@ Totality

13371329Idris distinguishes between *total* and *partial* functions.

13381330A total function is a function that either:

13391331

1340−+ Terminates for all possible inputs, or

1332++ Terminates for all possible inputs, or

13411333+ Produces a non-empty, finite, prefix of a possibly infinite result

13421334

13431335If a function is total, we can consider its type a precise description of what

@@ -1345,12 +1337,12 @@ that function will do. For example, if we have a function with a return

13451337type of ``String`` we know something different, depending on whether or not

13461338it's total:

13471339

1348−+ If it's total, it will return a value of type ``String`` in finite time

1340++ If it's total, it will return a value of type ``String`` in finite time;

13491341+ If it's partial, then as long as it doesn't crash or enter an infinite loop,

13501342 it will return a ``String``.

13511343

13521344Idris makes this distinction so that it knows which functions are safe to

1353−evaluate while type checking (as we've seen with :ref:`sect-fctypes`). After all,

1345+evaluate while type checking (as we've seen with :ref:`sect-fctypes`). After all,

13541346if it tries to evaluate a function during type checking which doesn't

13551347terminate, then type checking won't terminate!

13561348Therefore, only total functions will be evaluated during type checking.