7f6f3c4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Spelling in Sphinx documentation

Ran aspell over the documentation. Where there were conflicts between American and British spelling, picked the British variant, as most of it seemed to be written in that style. I don't really care, I'm American.

commit7f6f3c4693cd61b965f22412bfe0e6950db8d3b5 authorEcho Nolan <echo@echonolan.net> dateWed 2 Sep 2015, 14:02 (11 years ago) parentabac36e

23 files changed+41−41

compare with master

unifiedsplit

docs/effects/conclusions.rst+1−1

@@ -27,7 +27,7 @@ following places:

2727 protocol description language.

2828

2929The inspiration for the ``Effects`` library was Bauer and Pretnar’s

30−Eff language [2]_, which describes a langauge based on algebraic

30+Eff language [2]_, which describes a language based on algebraic

3131effects and handlers. Other recent languages and libraries have also

3232been built on this ideas, for example [3]_ and [4]_. The theoretical

3333foundations are also well-studied see [5]_, [6]_, [7]_, [8]_.

docs/effects/index.rst+1−1

@@ -10,7 +10,7 @@ A tutorial on the `Effects` package in `Idris`.

1010

1111 The documentation for Idris has been published under the Creative

1212 Commons CC0 License. As such to the extent possible under law, *The

13− Idris Community* has waived all copyright and related or neighboring

13+ Idris Community* has waived all copyright and related or neighbouring

1414 rights to Documentation for Idris.

1515

1616 More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

docs/effects/simpleeff.rst+3−3

@@ -120,7 +120,7 @@ Aside: Resource Types

120120---------------------

121121

122122To find out the resource type of an effect, if necessary (for example

123−if we want to initialise a resource explicitiy with ``runInit`` rather

123+if we want to initialise a resource explicitly with ``runInit`` rather

124124than using a default value with ``run``) we can run the

125125``resourceType`` function at the REPL:

126126

@@ -161,7 +161,7 @@ Suppose we have a ``String`` which is expected to represent an integer

161161in the range ``0`` to ``n``. We can write a function ``parseNumber``

162162which returns an ``Int`` if parsing the string returns a number in the

163163appropriate range, or throws an exception otherwise. Exceptions are

164−paramaterised by an error type:

164+parameterised by an error type:

165165

166166.. code-block:: idris

167167

@@ -542,7 +542,7 @@ which gives a random number up to a maximum value:

542542 | Random Integer

543543

544544Then, we need to deal with the new case, making sure that we extend

545−the list of events to include ``RND``. It doen’t matter where ``RND``

545+the list of events to include ``RND``. It doesn't matter where ``RND``

546546appears in the list, as long as it is present:

547547

548548.. code-block:: idris

docs/effects/state.rst+2−2

@@ -323,7 +323,7 @@ applying a function to the current state.

323323

324324Finally, our top level ``treeTag`` function now returns a pair of the

325325number of leaves, and the new tree. Resources for labelled effects are

326−intialised using the ``:=`` operator (reminisicent of assignment in an

326+initialised using the ``:=`` operator (reminiscent of assignment in an

327327imperative language):

328328

329329.. code-block:: idris

@@ -422,7 +422,7 @@ underlying type ``EffM``:

422422 -> (t -> List EFFECT) -> Type

423423

424424This is more general than the types we have been writing so far. It is

425−parameterised over an underying computation context ``m``, a

425+parameterised over an underlying computation context ``m``, a

426426result type ``t`` as we have already seen, as well as a ``List EFFECT`` and a

427427function type ``t -> List EFFECT``.

428428

docs/faq/faq.rst+4−4

@@ -119,7 +119,7 @@ argument which converges to a base case.

119119 higher order applications are not supported

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

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

122− ``k`` is syntactially smaller than ``S (S k)`` because ``k`` is a

122+ ``k`` is syntactically smaller than ``S (S k)`` because ``k`` is a

123123 subterm of ``S (S k)``, but ``(k, k)`` is

124124 not syntactically smaller than ``(S k, S k)``.

125125

@@ -147,8 +147,8 @@ Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64

147147

148148Historically the C language and many other languages have used the

149149names ``Float`` and ``Double`` to represent floating point numbers of

150−size 32 and 64 respectivly. Newer languages such as Rust and Julia

151−have begun to follow the naming scheme described in `IEE Standard for

150+size 32 and 64 respectively. Newer languages such as Rust and Julia

151+have begun to follow the naming scheme described in `IEEE Standard for

152152Floating-Point Arithmetic (IEEE 754)

153153<https://en.wikipedia.org/wiki/IEEE_floating_point>`_. This describes

154154single and double precision numbers as ``Float32`` and ``Float64``;

@@ -186,4 +186,4 @@ Where can I find more answers?

186186

187187There is an `Unofficial FAQ

188188<https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ>`_ on the wiki on

189−github which answers more technical questions and may be updated more often.

189+GitHub which answers more technical questions and may be updated more often.

docs/guides/type-providers-ffi.rst+1−1

@@ -267,7 +267,7 @@ Next, an Idris file to define our providers:

267267 bytesToType 2 = Provide (FIntT IT16)

268268 bytesToType 4 = Provide (FIntT IT32)

269269 bytesToType 8 = Provide (FIntT IT64)

270− bytesToType _ = Error "Unrecognized integral type."

270+ bytesToType _ = Error "Unrecognised integral type."

271271

272272 getDevT : IO (Provider FTy)

273273 getDevT = map bytesToType sizeOfDevT

docs/proofs/inductive.rst+1−1

@@ -13,7 +13,7 @@ numbers. Recall that they are defined recursively, as follows:

1313 S : Nat -> Nat

1414

1515A *total* function over natural numbers must both terminate, and cover

16−all possible inputs. Idris checks functions for totality by cheking that

16+all possible inputs. Idris checks functions for totality by checking that

1717all inputs are covered, and that all recursive calls are on

1818*structurally smaller* values (so recursion will always reach a base

1919case). Recalling ``plus``:

docs/proofs/interactive.rst+2−2

@@ -111,8 +111,8 @@ other required lemma, ``plusredZ_S``:

111111In this case, the goal is a function type, using ``k`` (the argument

112112accessible by pattern matching) and ``ih`` — the local variable

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

114−premisses using the ``intro`` tactic twice (or ``intros``, which

115−introduces all arguments as premisses). This gives:

114+premises using the ``intro`` tactic twice (or ``intros``, which

115+introduces all arguments as premises). This gives:

116116

117117.. code-block:: idris

118118

docs/proofs/patterns.rst+1−1

@@ -120,7 +120,7 @@ First, create a template definition with ``\d``:

120120 plus_commutes_Z = ?plus_commutes_Z_rhs

121121

122122Since we are going to write this by induction on ``m``, which is

123−implciit, we will need to bring ``m`` into scope manually:

123+implicit, we will need to bring ``m`` into scope manually:

124124

125125.. code-block:: idris

126126

docs/reference/compilation.rst+1−1

@@ -51,7 +51,7 @@ Idris supports the logging at various different levels of verbosity: 1 to 10.

5151+ Level 0: Show no logging output. Default level

5252+ Level 1: High level details of the compilation process.

5353+ Level 2: Provides details of the coverage checking, and further details the elaboration process specifically: Class, Clauses, Data, Term, and Types,

54−+ Level 3: Provides details of compilation of the IRTS, erasue, parsing, case splitting, and further details elaboration of: Instances, Providers, and Values.

54++ Level 3: Provides details of compilation of the IRTS, erasure, parsing, case splitting, and further details elaboration of: Instances, Providers, and Values.

5555+ Level 4: Provides further details on: Erasure, Coverage Checking, Case splitting, and elaboration of clauses.

5656+ Level 5: Provides details on the prover, and further details elaboration (adding declarations) and compilation of the IRTS.

5757+ Level 6: Further details elaboration and coverage checking.

docs/reference/documenting.rst+3−3

@@ -40,7 +40,7 @@ lines, each of which begins with ``|||`` (three pipe symbols). The

4040first paragraph of the documentation is taken to be an overview, and

4141in some contexts, only this overview will be shown. After the

4242documentation for the declaration as a whole, it is possible to

43−associate documetation with specific named parameters, which can

43+associate documentation with specific named parameters, which can

4444either be explicitly name or the results of converting free variables

4545to implicit parameters. Annotations are the same as with Javadoc

4646annotations, that is for the named parameter ``(n : T)``, the

@@ -75,7 +75,7 @@ italics correctly). A comprehensive set of examples is given below.

7575 ||| Append some vectors

7676 ||| @ a the contents of the vectors

7777 ||| @ xs the first vector (recursive param)

78− ||| @ ys the second vector (not analyzed)

78+ ||| @ ys the second vector (not analysed)

7979 appendV : (xs : Vect n a) -> (ys : Vect m a) -> Vect (add n m) a

8080 appendV [] ys = ys

8181 appendV (x::xs) ys = x :: appendV xs ys

@@ -98,7 +98,7 @@ italics correctly). A comprehensive set of examples is given below.

9898 ||| @ ty the type of the term

9999 data Term : (ctxt : Vect n Ty) -> (ty : Ty) -> Type where

100100

101− ||| The consructor of the unit type

101+ ||| The constructor of the unit type

102102 ||| More comment

103103 ||| @ ctxt the typing context

104104 UnitCon : {ctxt : Vect n Ty} -> Term ctxt UNIT

docs/reference/elaborator-reflection.rst+1−1

@@ -147,7 +147,7 @@ Recursive Elaboration

147147=====================

148148

149149The elaboration mechanism can be invoked recursively using the ``runElab`` tactic.

150−This tactic takes a goal type and an elaboration script as arguments and runs the script in a fresh lexical evironment to create an inhabitant of the provided goal type.

150+This tactic takes a goal type and an elaboration script as arguments and runs the script in a fresh lexical environment to create an inhabitant of the provided goal type.

151151This is primarily useful for code generation, particularly for generating pattern-matching clauses, where variable scope needs to be one that isn't the present local context.

152152

153153Learn More

docs/reference/erasure.rst+2−2

@@ -95,7 +95,7 @@ cannot get below O(n) with time complexities.

9595One could argue that Idris in fact compiles ``Nat`` via GMP but

9696that's a moot point for two reasons:

9797

98−+ First, whenever we try to index our datastructures with anything

98++ First, whenever we try to index our data structures with anything

9999 else than ``Nat``, the compiler is not going to come to the rescue.

100100

101101+ Second, even with ``Nat``, the GMP integers are *still* there and

@@ -277,7 +277,7 @@ has a slightly different meaning. We need more consistent and

277277understandable naming.

278278

279279If the same type is used in both erased and non-erased context, it

280−will retain its fields to accomodate the least common denominator --

280+will retain its fields to accommodate the least common denominator --

281281the non-erased context. This is particularly troublesome in the case

282282of the type of (dependent) pairs, where it actually means that no

283283erasure would be performed. We should probably locate disjoint uses of

docs/reference/ide-protocol.rst+3−3

@@ -40,7 +40,7 @@ The syntax is::

4040where ``NUM`` is either 0 or a positive integer, ``ALPHA`` is an alphabetical character, and ``STR`` is the contents of a string, with ``"`` escaped by a backslash.

4141The atom ``nil`` is accepted instead of ``()`` for compatibility with some regexp pretty-printing routines.

4242

43−The state of the Idris process is mainly the active file, which needs to be kept synchronized between the editor and Idris.

43+The state of the Idris process is mainly the active file, which needs to be kept synchronised between the editor and Idris.

4444This is achieved by the already seen ``:load-file`` command.

4545

4646The available commands include:

@@ -184,12 +184,12 @@ The following keys are available:

184184 states that the region is antiquoted.

185185

186186 ``tt-term``

187− A serialized representation of the Idris core term corresponding to the region of text.

187+ A serialised representation of the Idris core term corresponding to the region of text.

188188

189189Source Code Highlighting

190190------------------------

191191

192−Idris supports instructing editors how to color their code.

192+Idris supports instructing editors how to colour their code.

193193When elaborating source code or REPL input, Idris will locate regions of the source code corresponding to names, and emit information about these names using the same metadata as output highlighting.

194194

195195These messages will arrive as replies to the command that caused elaboration to occur, such as ``:load-file`` or ``:interpret``.

docs/reference/language-features.rst+2−2

@@ -27,7 +27,7 @@ Core Language Features

2727- Heterogeneous equality

2828- ``do`` notation

2929- Idiom brackets

30−- Type classes, suppoting default methods and dependencies between

30+- Type classes, supporting default methods and dependencies between

3131 methods

3232- ``rewrite`` prf ``in`` expr

3333- Metavariables

@@ -35,7 +35,7 @@ Core Language Features

3535- Implicit coercion

3636- ``codata``

3737- Also ``Inf : Type -> Type`` type constructor for mixed data/codata.

38− In fact ``codata`` is implemented by putting recusive arguments under

38+ In fact ``codata`` is implemented by putting recursive arguments under

3939 ``Inf``.

4040- ``syntax`` rules for defining pattern and term syntactic sugar

4141- these are used in the standard library to define

docs/reference/packages.rst+1−1

@@ -92,7 +92,7 @@ Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler

9292

9393+ ``idris --checkpkg test.ipkg`` will type check all modules in the package only. This differs from build that type checks **and** generates code.

9494

95−+ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` paramater.

95++ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` parameter.

9696

9797Once the test package has been installed, the command line option

9898``--package test`` makes it accessible (abbreviated to ``-p test``).

docs/reference/syntax-guide.rst+2−2

@@ -60,8 +60,8 @@ or

6060 data List a = Nil | (::) a (List a)

6161

6262The second, more general kind of data type, is defined using Agda or

63−GADT style syntax. This syntax defines a data type that is parameterized

64−by some values (in the ``Vect`` exampe, a value of type ``Nat`` and a

63+GADT style syntax. This syntax defines a data type that is parameterised

64+by some values (in the ``Vect`` example, a value of type ``Nat`` and a

6565value of type ``Type``).

6666

6767.. code:: idris

docs/reference/tactics.rst+2−2

@@ -30,8 +30,8 @@ Commonly Used Tactics

3030Compute

3131-------

3232

33−- ``compute`` - Normalizes all terms in the goal (note: does not

34− normalize assumptions)

33+- ``compute`` - Normalises all terms in the goal (note: does not

34+ normalise assumptions)

3535

3636::

3737

docs/tutorial/classes.rst+2−2

@@ -146,7 +146,7 @@ give the constraints on the type variables left of the fat arrow

146146 sort : Ord a => List a -> List a

147147

148148Functions, classes and instances can have multiple

149−constraints. Multiple constaints are written in brackets in a comma

149+constraints. Multiple constraints are written in brackets in a comma

150150separated list, for example:

151151

152152.. code-block:: idris

@@ -511,7 +511,7 @@ parameter* of the ``MonadState`` class, because it is the parameter

511511used to resolve an instance.

512512

513513

514−.. [1] Conor Mcbride and Ross Paterson. 2008. Applicative programming

514+.. [1] Conor McBride and Ross Paterson. 2008. Applicative programming

515515 with effects. J. Funct. Program. 18, 1 (January 2008),

516516 1-13. DOI=10.1017/S0956796807006326

517517 http://dx.doi.org/10.1017/S0956796807006326

docs/tutorial/interactive.rst+2−2

@@ -171,7 +171,7 @@ then ``:ps 96 vzipWith_rhs_1`` will give

171171 []

172172

173173This works because it is searching for a ``Vect`` of length 0, of

174−which the empty vector is the only possibiliy. Similarly, and perhaps

174+which the empty vector is the only possibility. Similarly, and perhaps

175175surprisingly, there is only one possibility if we try to solve ``:ps

17617697 vzipWith_rhs_2``:

177177

@@ -254,5 +254,5 @@ There are also commands to invoke the type checker and evaluator:

254254- ``\r`` reloads and type checks the buffer.

255255

256256Corresponding commands are also available in the Emacs mode. Support

257−for other editors can be added in a relatively straighforward manner

257+for other editors can be added in a relatively straightforward manner

258258by using ``idris –client``.

docs/tutorial/packages.rst+1−1

@@ -55,7 +55,7 @@ Given an Idris package file ``maths.ipkg`` it can be used with the Idris compile

5555 generates code.

5656

5757+ ``idris --testpkg maths.ipkg`` will compile and run any embedded

58− tests you have specified in the ``tests`` paramater. More

58+ tests you have specified in the ``tests`` parameter. More

5959 information about testing is given in the next section.

6060

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

docs/tutorial/theorems.rst+1−1

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

113113 plusReducesS Z m = Refl

114114 plusReducesS (S k) m = cong (plusReducesS k m)

115115

116−Even for trival theorems like these, the proofs are a little tricky to

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

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

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

119119mode’.

docs/tutorial/typesfuns.rst+2−2

@@ -40,7 +40,7 @@ modules and the definitions in each module each have their own

4040namespace. This is discussed further in Section

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

4242definitions are given and indentation are significant. Functions and

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

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

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

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

4646same level of indentation as the preceding declaration.

@@ -1024,7 +1024,7 @@ Foe example:

10241024 className : String

10251025

10261026**Note** that it is no longer possible to use the ``addStudent``

1027−method from earlier as that would change the size of the class. To provide an add student the function must specify in the type that the size of the class has been increased by one. As the size if specified using natural numbers, the new value can be incremeated using the successor constructor.

1027+method from earlier as that would change the size of the class. To provide an add student the function must specify in the type that the size of the class has been increased by one. As the size if specified using natural numbers, the new value can be incremented using the successor constructor.

10281028

10291029.. code-block:: idris

10301030