idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Update docs

Browse Source
This commit is contained in:
Kamil Shakirov 2020-06-30 18:44:36 +06:00
parent df60e07962
commit f094a52ba9
3 changed files with 6 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
docs/source/listing/idris-prompt-helloworld.txt
View File

@ -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!

3
docs/source/tutorial/starting.rst
View File

@ -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!

8
docs/source/tutorial/typesfuns.rst
View File

@ -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