8a25f65 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Couple of small tutorial typos were fixed.

commit8a25f6503dab6a9488c7ff132e4447932a1aca86 authorDenis Buzdalov <public@buzden.ru> dateFri 4 Oct 2019, 22:11 (7 years ago) parent5965fb1

2 files changed+2−2

unifiedsplit

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