d4e7ead · Idris-dev · git.iko.soy

docs/effects/depeff.rst+2−2

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

43

44.. code-block:: idris

45

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

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

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

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

48 readInt = do let x = trim !getStr

49 putM (cast x :: !get)

50

docs/tutorial/miscellany.rst+1−1

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

242Testing foreign function calls

243------------------------------

244

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

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

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

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

248``%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:

1190 fst : a

1191 snd : b

1192

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

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

1195the record with the size. For example:

1196