f8c2edf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix reST errors.

commitf8c2edf0b21494699321314180e2746bcdf6034a authorJan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk> dateThu 9 Nov 2017, 13:14 (9 years ago) parent3292691

6 files changed+29−32

compare with master

unifiedsplit

docs/faq/faq.rst+5−4 docs/proofs/inductive.rst+2 docs/st/state.rst+15−17 docs/tutorial/interfaces.rst+6−6 docs/tutorial/modules.rst−4 docs/tutorial/starting.rst+1−1

docs/faq/faq.rst+5−4

@@ -137,7 +137,7 @@ of ``append``, rather than making the type of ``append`` equivalent to...

137137

138138...which is probably not what was intended! The reason for this rule is so

139139that it is clear just from looking at the type of ``append``, and no other

140−context, what the implicitly bound names are.

140+context, what the implicitly bound names are.

141141

142142If you want to use an unapplied name in a type, you have two options. You

143143can either explicitly qualify it, for example, if ``ty`` is defined in the

@@ -149,7 +149,7 @@ namespace ``Main`` you can do the following:

149149

150150Alternatively, you can use a name which does not begin with a lower case

151151letter, which will never be implicitly bound:

152−

152+

153153.. code-block:: idris

154154

155155 Ty : Type

@@ -283,8 +283,9 @@ This answer is based on Edwin Brady's response in the following

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

284284

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

286−=======================================

287−The Idris Community Standards are stated `here

286+==================================================================

287+

288+The Idris Community Standards are stated `here

288289<https://www.idris-lang.org/documentation/community-standards/>`_ .

289290

290291Where can I find more answers?

docs/proofs/inductive.rst+2

@@ -1,3 +1,5 @@

1+.. _sect-inductive:

13****************

24Inductive Proofs

35****************

docs/st/state.rst+15−17

@@ -19,10 +19,10 @@ how those resources change when a function runs:

1919 Type

2020

2121A value of type ``STrans m resultType in_res out_res_fn`` represents a sequence

22−of actions which can manipulate state. The arguments are:

22+of actions which can manipulate state. The arguments are:

2323

2424* ``m``, which is an underlying *computation context* in which the actions will be executed.

25− Usually, this will be a generic type with a ``Monad`` implementation, but

25+ Usually, this will be a generic type with a ``Monad`` implementation, but

2626 it isn't necessarily so. In particular, there is no need to understand monads

2727 to be able to use ``ST`` effectively!

2828* ``resultType``, which is the type of the value the sequence will produce

@@ -76,10 +76,10 @@ resource is still a ``State Integer`` on output:

7676 same. We'll introduce a much more concise way of writing this type at the

7777 end of this section (:ref:`sttype`), when we describe the ``ST`` type

7878 itself.

79−

79+

8080This function reads the value stored at the resource ``x`` with ``read``,

8181increments it then writes the result back into the resource ``x`` with

82−``write``. We'll see the types of ``read`` and ``write`` shortly

82+``write``. We'll see the types of ``read`` and ``write`` shortly

8383(see :ref:`stransprimops`). We can also create and delete resources:

8484

8585.. code-block:: idris

@@ -104,7 +104,7 @@ can run it in *any* context. We can run it in the identity context with

104104``runPure``. For example, try entering the above definitions in a file

105105``Intro.idr`` then running the following at the REPL:

106106

107−.. code::

107+.. code::

108108

109109 *Intro> runPure (makeAndIncrement 93)

110110 94 : Integer

@@ -179,7 +179,7 @@ of ``lift`` shortly.

179179 Conceptually, at least, you can think of it as having the following type:

180180

181181 .. code-block:: idris

182−

182+

183183 (!) : STrans m a state_in state_out -> a

184184

185185 It is syntactic sugar for binding a variable immediately before the

@@ -243,7 +243,7 @@ context. Here, we use ``run``, which allows us to execute an ``STrans`` program

243243in any context (as long as it has an implementation of ``Applicative``) and we

244244can execute ``ioMakeAndIncrement`` at the REPL as follows:

245245

246−.. code::

246+.. code::

247247

248248 *Intro> :exec run ioMakeAndIncrement

249249 Enter a number: 93

@@ -269,7 +269,7 @@ its length will change:

269269 addElement vec item = do xs <- read vec

270270 write vec (item :: xs)

271271

272−Note that you'll need to ``import Data.Vect`` to try this example.

272+Note that you'll need to ``import Data.Vect`` to try this example.

273273

274274.. topic:: Updating a state directly with ``update``

275275

@@ -344,7 +344,7 @@ if the input is valid. We can express this in the type as follows:

344344Then, when we implement ``readAndAdd`` we need to return the appropriate

345345value for the output state. If we've added an item to the vector, we need to

346346return ``True``, otherwise we need to return ``False``:

347−

347+

348348.. code-block:: idris

349349

350350 readAndAdd : ConsoleIO io => (vec : Var) ->

@@ -435,7 +435,7 @@ we can do as follows:

435435

436436.. _stransprimops:

437437

438−``STrans`` Primitive operations

438+``STrans`` Primitive operations

439439===============================

440440

441441Now that we've written a few small examples of ``STrans`` functions, it's

@@ -485,7 +485,7 @@ of type ``State state``:

485485

486486.. code-block:: idris

487487

488− new : (val : state) ->

488+ new : (val : state) ->

489489 STrans m Var res (\lbl => (lbl ::: State state) :: res)

490490

491491It's important that the new resource has type ``State state``, rather than

@@ -526,7 +526,7 @@ the resource list so that it is appropriate for returning that value:

526526

527527.. code-block:: idris

528528

529− returning : (result : ty) ->

529+ returning : (result : ty) ->

530530 STrans m () res (const (out_fn result)) ->

531531 STrans m ty res out_fn

532532

@@ -555,7 +555,7 @@ programming and reasoning in Idris.

555555.. _sttype:

556556

557557`ST`: Representing state transitions directly

558−============================================

558+=============================================

559559

560560We've seen a few examples of small ``STrans`` functions now, and

561561their types can become quite verbose given that we need to provide explicit

@@ -568,7 +568,7 @@ giving input and output resource lists in full. We can do this with

568568.. code-block:: idris

569569

570570 ST : (m : Type -> Type) ->

571− (resultType : Type) ->

571+ (resultType : Type) ->

572572 List (Action resultType) -> Type

573573

574574``ST`` is a type level function which computes an appropriate ``STrans``

@@ -593,7 +593,7 @@ So, we can write some of the function types we've seen so far as follows:

593593That is, ``increment`` begins and ends with ``x`` in state ``State Integer``.

594594

595595.. code-block:: idris

596−

596+

597597 makeAndIncrement : Int -> ST m Int []

598598

599599That is, ``makeAndIncrement`` begins and ends with no resources.

@@ -652,5 +652,3 @@ the rare occasions we need the full precision of ``STrans``. In the next

652652section, we'll see how to use the facilities provided by ``ST`` to write

653653a precise API for a system with security properties: a data store requiring

654654a login.

655−

656−

docs/tutorial/interfaces.rst+6−6

@@ -48,7 +48,7 @@ For example, the

4848Only one implementation of an interface can be given for a type — implementations may

4949not overlap. Implementation declarations can themselves have constraints.

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

51−constructors (either data or type constructors) or variables

51+constructors (either data or type constructors) or variables

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

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

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

@@ -157,7 +157,7 @@ Note: Interfaces and ``mutual`` blocks

157157~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

158158

159159Idris is strictly "define before use", except in ``mutual`` blocks.

160−In a ``mutual`` block, Idris elaborates in two passes: types on the first

160+In a ``mutual`` block, Idris elaborates in two passes: types on the first

161161pass and definitions on the second. When the mutual block contains an

162162interface declaration, it elaborates the interface header but none of the

163163method types on the first pass, and elaborates the method types and any

@@ -259,7 +259,7 @@ are both available, or return ``Nothing`` if one or both are not ("fail fast").

259259 Nothing : Maybe Int

260260

261261Pattern Matching Bind

262−---------------------

262+~~~~~~~~~~~~~~~~~~~~~

263263

264264Sometimes we want to pattern match immediately on the result of a function

265265in ``do`` notation. For example, let's say we have a function ``readNumber``

@@ -323,7 +323,7 @@ of the ``do`` block. The second part gives the alternative bindings, of which

323323there may be more than one.

324324

325325``!``-notation

326−--------------

326+~~~~~~~~~~~~~~

327327

328328In many cases, using ``do``-notation can make programs unnecessarily

329329verbose, particularly in cases such as ``m_add`` above where the value

@@ -367,7 +367,7 @@ is lifted to:

367367 f g'

368368

369369Monad comprehensions

370−--------------------

370+~~~~~~~~~~~~~~~~~~~~

371371

372372The list comprehension notation we saw in Section

373373:ref:`sect-more-expr` is more general, and applies to anything which

@@ -461,7 +461,7 @@ application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>

461461 m_add' x y = [| x + y |]

462462

463463An error-handling interpreter

464−-----------------------------

464+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

465465

466466Idiom notation is commonly useful when defining evaluators. McBride

467467and Paterson describe such an evaluator [1]_, for a language similar

docs/tutorial/modules.rst−4

@@ -189,8 +189,6 @@ the ``public`` modifier on an ``import``. For example:

189189 import B

190190 import public C

191191

192− public a : AType a = ...

193−

194192The module ``A`` will export the name ``a``, as well as any public or

195193abstract names in module ``C``, but will not re-export anything from

196194module ``B``.

@@ -277,5 +275,3 @@ which can be inferred by the type checker:

277275

278276 *params> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))

279277 "[1, 2, 3, 4, 5, 6]" : String

280−

281−

docs/tutorial/starting.rst+1−1

@@ -11,7 +11,7 @@ Before installing Idris, you will need to make sure you have all

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

1212

1313- A fairly recent version of `GHC <https://www.haskell.org/ghc/>`_. The

14− earliest version we currently test with is 7.6.3.

14+ earliest version we currently test with is 7.10.3.

1515

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

1717