d4e7ead · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #4768 from buzden/tutorial-typo-fix

Couple of typo fixes in tutorial

commitd4e7ead1be8f14655e953447dfb517d1b58f33a6 authorNiklas Larsson <metaniklas@gmail.com> dateMon 21 Oct 2019, 13:31 (7 years ago) parent3257106 7f4ee1f

3 files changed+4−4

compare with master

unifiedsplit

docs/effects/depeff.rst+2−2 docs/tutorial/miscellany.rst+1−1 docs/tutorial/typesfuns.rst+1−1

docs/effects/depeff.rst+2−2

@@ -43,8 +43,8 @@ express this as follows:

4343

4444.. code-block:: idris

4545

46− readInt : Eff ()[STATE (Vect n Int), STDIO]

47− [STATE (Vect (S n) Int), STDIO]

46+ readInt : Eff () [STATE (Vect n Int), STDIO]

47+ [STATE (Vect (S n) Int), STDIO]

4848 readInt = do let x = trim !getStr

4949 putM (cast x :: !get)

5050

docs/tutorial/miscellany.rst+1−1

@@ -242,7 +242,7 @@ through the following directives:

242242Testing foreign function calls

243243------------------------------

244244

245−Normally, the Idris interpreter (used for typechecking and at the REPL)

245+Normally, the Idris interpreter (used for typechecking and as the REPL)

246246will not perform IO actions. Additionally, as it neither generates C

247247code nor compiles to machine code, the ``%lib``, ``%include`` and

248248``%link`` directives have no effect. IO actions and FFI calls can be

docs/tutorial/typesfuns.rst+1−1

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

11901190 fst : a

11911191 snd : b

11921192

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

1193+Using the ``Class`` record from earlier, the size of the class can be

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

11951195the record with the size. For example:

11961196