From 0ea595817ac6d02d4da59eba6a226932d82bb74e Mon Sep 17 00:00:00 2001
From: Kamil Shakirov <kamils80@gmail.com>
Date: Thu, 9 Apr 2020 13:48:12 +0600
Subject: [PATCH] Fix some typos in the tutorial

---
 docs/tutorial/interfaces.rst |  8 +++++---
 docs/tutorial/typesfuns.rst  | 10 +++-------
 2 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/docs/tutorial/interfaces.rst b/docs/tutorial/interfaces.rst
index e754064..65a3f43 100644
--- a/docs/tutorial/interfaces.rst
+++ b/docs/tutorial/interfaces.rst
@@ -282,11 +282,13 @@ which reads a number from the console, returning a value of the form
 
 .. code-block:: idris
 
+    import Data.Strings
+
     readNumber : IO (Maybe Nat)
     readNumber = do
       input <- getLine
       if all isDigit (unpack input)
-         then pure (Just (cast input))
+         then pure (Just (stringToNatOrZ input))
          else pure Nothing
 
 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
-      = do Just x_ok <- readNumber 
+      = do Just x_ok <- readNumber
                 | Nothing => pure Nothing
-           Just y_ok <- readNumber 
+           Just y_ok <- readNumber
                 | Nothing => pure Nothing
            pure (Just (x_ok, y_ok))
 
diff --git a/docs/tutorial/typesfuns.rst b/docs/tutorial/typesfuns.rst
index fa9d369..f24469e 100644
--- a/docs/tutorial/typesfuns.rst
+++ b/docs/tutorial/typesfuns.rst
@@ -221,12 +221,12 @@ of how this works in practice:
       odd : Nat -> Bool
       odd Z = False
       odd (S k) = even k
-    
+
     test : List Nat
     test = [c (S 1), c Z, d (S Z)]
       where c : Nat -> Nat
             c x = 42 + x
-    
+
             d : Nat -> Nat
             d y = c (y + 1 + z y)
                   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/Vect.idr``
 
--  ``libs/base/Data/VectType.idr``
-
 Functions include filtering, appending, reversing, and so on.
 
 Aside: Anonymous functions and operator sections
@@ -1052,7 +1048,7 @@ name. For example, a pair type could be defined as follows:
         fst : a
         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
 the record with the size.  For example: