Idris2/docs/source/listing/idris-prompt-start.txt

$ idris2
     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.7.0
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main>
Copy more files over from Idris2 2020-05-20 13:23:04 +03:00			`$ idris2`
			`____ __ _ ___`
			`/ _/___/ /____(_)____ \|__ \`
[ rc ] Prepare for 0.7.0 A lot more sensible all around : ) 2023-12-21 14:04:03 +03:00			`/ // __ / ___/ / ___/ __/ / Version 0.7.0`
Copy more files over from Idris2 2020-05-20 13:23:04 +03:00			`_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org`
			`/___/\__,_/_/ /_/____/ /____/ Type :? for help`

			`Welcome to Idris 2. Enjoy yourself!`
			`Main>`