22ef96b · Idris-dev · git.iko.soy

docs/effects/index.rst+1−1

compare with master

unifiedsplit

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

10

11 The documentation for Idris has been published under the Creative

12 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

14 rights to Documentation for Idris.

15

16 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

120---------------------

121

122To 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

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

125``resourceType`` function at the REPL:

126

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

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

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

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

164−paramaterised by an error type:

164+parameterised by an error type:

165

166.. code-block:: idris

167

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

542 | Random Integer

543

544Then, 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``

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

547

548.. code-block:: idris

docs/effects/state.rst+2−2

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

323

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

325number 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

327imperative language):

328

329.. code-block:: idris

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

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

423

424This 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

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

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

428

docs/faq/faq.rst+4−4

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

119 higher order applications are not supported

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

121 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

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

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

125

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

147

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

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

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

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

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

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

152Floating-Point Arithmetic (IEEE 754)

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

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

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

186

187There is an `Unofficial FAQ

188<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:

267 bytesToType 2 = Provide (FIntT IT16)

268 bytesToType 4 = Provide (FIntT IT32)

269 bytesToType 8 = Provide (FIntT IT64)

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

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

271

272 getDevT : IO (Provider FTy)

273 getDevT = map bytesToType sizeOfDevT

docs/proofs/inductive.rst+1−1

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

13 S : Nat -> Nat

14

15A *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

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

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

19case). Recalling ``plus``:

docs/proofs/interactive.rst+2−2

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

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

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

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

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

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

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

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

116

117.. code-block:: idris

118

docs/proofs/patterns.rst+1−1

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

120 plus_commutes_Z = ?plus_commutes_Z_rhs

121

122Since 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:

124

125.. code-block:: idris

126

docs/reference/compilation.rst+1−1

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

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

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

53+ 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.

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

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

57+ 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

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

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

42documentation 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

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

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

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

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

75 ||| Append some vectors

76 ||| @ a the contents of the vectors

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

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

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

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

80 appendV [] ys = ys

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

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

98 ||| @ ty the type of the term

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

100

101− ||| The consructor of the unit type

101+ ||| The constructor of the unit type

102 ||| More comment

103 ||| @ ctxt the typing context

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

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

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

147=====================

148

149The 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.

151This 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.

152

153Learn More

docs/reference/erasure.rst+2−2

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

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

96that's a moot point for two reasons:

97

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

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

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

100

101+ 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

277understandable naming.

278

279If 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 --

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

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

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

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

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

40where ``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.

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

42

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.

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

45

46The available commands include:

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

184 states that the region is antiquoted.

185

186 ``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.

188

189Source Code Highlighting

190------------------------

191

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

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

193When 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.

194

195These 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

27- Heterogeneous equality

28- ``do`` notation

29- Idiom brackets

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

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

31 methods

32- ``rewrite`` prf ``in`` expr

33- Metavariables

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

35- Implicit coercion

36- ``codata``

37- 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

39 ``Inf``.

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

41- 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

92

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

94

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.

96

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

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

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

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

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

61

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

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

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

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

65value of type ``Type``).

66

67.. code:: idris

docs/reference/tactics.rst+2−2

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

30Compute

31-------

32

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

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

34− normalize assumptions)

34+ normalise assumptions)

35

36::

37

docs/tutorial/classes.rst+2−2

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

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

147

148Functions, 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

150separated list, for example:

151

152.. code-block:: idris

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

511used to resolve an instance.

512

513

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

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

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

516 1-13. DOI=10.1017/S0956796807006326

517 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

171 []

172

173This 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

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

17697 vzipWith_rhs_2``:

177

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

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

255

256Corresponding 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

258by 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

55 generates code.

56

57+ ``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

59 information about testing is given in the next section.

60

61Once 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:

113 plusReducesS Z m = Refl

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

115

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

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

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

119mode’.

docs/tutorial/typesfuns.rst+6−6

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

40namespace. This is discussed further in Section

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

42definitions 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

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

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

46same level of indentation as the preceding declaration.

@@ -901,10 +901,10 @@ Records

901

902*Records* are data types which collect several values (the record's

903*fields*) together. Idris provides syntax for defining records and

904−*automatically generating field access and update functions*. Unlike

904+automatically generating field access and update functions. Unlike

905−*the syntax used for data structures, records in Idris follow a

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

906−*different syntax to that seen with Haskell. For example, we can

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

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

907+represent a person's name and age in a record:

908

909.. code-block:: idris

910

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

1024 className : String

1025

1026**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.

1028

1029.. code-block:: idris

1030