mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-27 18:53:42 +03:00
fix typo in docs/tutorial/typesfuns.rst
duplicated word
This commit is contained in:
parent
59503712f3
commit
e6fe418a6b
@ -565,7 +565,7 @@ We can also read strings from user input:
|
||||
|
||||
A number of other I/O operations are available. For example, by adding
|
||||
``import System.File`` to your program, you get access to functions for
|
||||
for reading and writing files, including:
|
||||
reading and writing files, including:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user