diff --git a/docs/source/listing/idris-prompt-helloworld.txt b/docs/source/listing/idris-prompt-helloworld.txt
index c32f2039b..a0ecec1e5 100644
--- a/docs/source/listing/idris-prompt-helloworld.txt
+++ b/docs/source/listing/idris-prompt-helloworld.txt
@@ -9,7 +9,6 @@ Welcome to Idris 2.  Enjoy yourself!
 Main> :t main
 Main.main : IO ()
 Main> :c hello main
-compiling hello.ss with output to hello.so
-File hello.so written
+File build/exec/hello written
 Main> :q
 Bye for now!
diff --git a/docs/source/tutorial/starting.rst b/docs/source/tutorial/starting.rst
index 3eafc6168..7d01168d4 100644
--- a/docs/source/tutorial/starting.rst
+++ b/docs/source/tutorial/starting.rst
@@ -87,8 +87,7 @@ which you can run:
 ::
 
     $ idris2 hello.idr -o hello
-    compiling hello.ss with output to hello.so
-    $ ./build/exec/hello.so
+    $ ./build/exec/hello
     Hello world
 
 Please note that the dollar sign ``$`` indicates the shell prompt!
diff --git a/docs/source/tutorial/typesfuns.rst b/docs/source/tutorial/typesfuns.rst
index c918bc141..a171b7d4b 100644
--- a/docs/source/tutorial/typesfuns.rst
+++ b/docs/source/tutorial/typesfuns.rst
@@ -143,9 +143,9 @@ We can test these functions at the Idris prompt:
 ::
 
     Main> plus (S (S Z)) (S (S Z))
-    S (S (S (S Z)))
+    4
     Main> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
-    S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))
+    12
 
 Like arithmetic operations, integer literals are also overloaded using
 interfaces, meaning that we can also test the functions as follows:
@@ -153,9 +153,9 @@ interfaces, meaning that we can also test the functions as follows:
 ::
 
     Idris> plus 2 2
-    S (S (S (S Z)))
+    4
     Idris> mult 3 (plus 2 2)
-    S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))
+    12
 
 You may wonder, by the way, why we have unary natural numbers when our
 computers have perfectly good integer arithmetic built in. The reason