edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-24 04:43:25 +03:00
Code Issues Projects Releases Wiki Activity

Fix some typos in the tutorial

Browse Source
This commit is contained in:
Kamil Shakirov 2020-04-09 13:48:12 +06:00
parent 211fc359ca
commit 0ea595817a
2 changed files with 8 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
docs/tutorial/interfaces.rst
View File

@ -282,11 +282,13 @@ which reads a number from the console, returning a value of the form
.. code-block:: idris .. code-block:: idris
import Data.Strings
readNumber : IO (Maybe Nat) readNumber : IO (Maybe Nat)
readNumber = do readNumber = do
input <- getLine input <- getLine
if all isDigit (unpack input) if all isDigit (unpack input)
then pure (Just (cast input)) then pure (Just (stringToNatOrZ input))
else pure Nothing else pure Nothing
If we then use it to write a function to read two numbers, returning If we then use it to write a function to read two numbers, returning
@ -325,9 +327,9 @@ case back as follows:
readNumbers : IO (Maybe (Nat, Nat)) readNumbers : IO (Maybe (Nat, Nat))
readNumbers readNumbers
= do Just x_ok <- readNumber = do Just x_ok <- readNumber
| Nothing => pure Nothing | Nothing => pure Nothing
Just y_ok <- readNumber Just y_ok <- readNumber
| Nothing => pure Nothing | Nothing => pure Nothing
pure (Just (x_ok, y_ok)) pure (Just (x_ok, y_ok))

10
docs/tutorial/typesfuns.rst
View File

@ -221,12 +221,12 @@ of how this works in practice:
odd : Nat -> Bool odd : Nat -> Bool
odd Z = False odd Z = False
odd (S k) = even k odd (S k) = even k
test : List Nat test : List Nat
test = [c (S 1), c Z, d (S Z)] test = [c (S 1), c Z, d (S Z)]
where c : Nat -> Nat where c : Nat -> Nat
c x = 42 + x c x = 42 + x
d : Nat -> Nat d : Nat -> Nat
d y = c (y + 1 + z y) d y = c (y + 1 + z y)
where z : Nat -> Nat where z : Nat -> Nat
@ -753,12 +753,8 @@ For more details of the functions available on ``List`` and
- ``libs/base/Data/List.idr`` - ``libs/base/Data/List.idr``
- ``libs/base/Data/List.idr``
- ``libs/base/Data/Vect.idr`` - ``libs/base/Data/Vect.idr``
- ``libs/base/Data/VectType.idr``
Functions include filtering, appending, reversing, and so on. Functions include filtering, appending, reversing, and so on.
Aside: Anonymous functions and operator sections Aside: Anonymous functions and operator sections
@ -1052,7 +1048,7 @@ name. For example, a pair type could be defined as follows:
fst : a fst : a
snd : b snd : b
Using the ``class`` record from earlier, the size of the class can be Using the ``Class`` record from earlier, the size of the class can be
restricted using a ``Vect`` and the size included in the type by parameterising restricted using a ``Vect`` and the size included in the type by parameterising
the record with the size. For example: the record with the size. For example: