edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-25 22:06:33 +03:00
Code Issues Projects Releases Wiki Activity

Update Idris prompt in the tutorial

Browse Source
This commit is contained in:
Kamil Shakirov 2020-04-03 16:44:12 +06:00
parent 59503712f3
commit 55b3f880d3
3 changed files with 13 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
docs/listing/idris-prompt-helloworld.txt
View File

@ -1,9 +1,9 @@
$ idris hello.idr
____ __ _ ___
/ _/___/ /____(_)____ |__ \
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.1.0
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help
Welcome to Idris 2. Enjoy yourself!
Main> :t main

9
docs/listing/idris-prompt-interp.txt
View File

@ -1,12 +1,11 @@
$ idris2 interp.idr
____ __ _ ___
/ _/___/ /____(_)____ |__ \
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.1.0
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help
Welcome to Idris 2. Enjoy yourself!
Main> :exec main
Enter a number: 6
720

10
docs/listing/idris-prompt-start.txt
View File

@ -1,9 +1,9 @@
$ idris2
____ __ _ ___
/ _/___/ /____(_)____ |__ \
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.1.0
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help
Welcome to Idris 2. Enjoy yourself!
Main>
Main>