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

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

Welcome to Idris 2.  Enjoy yourself!
Main> :exec main
Enter a number: 6
720
Copy more files over from Idris2 2020-05-20 13:23:04 +03:00			`$ idris2 interp.idr`
			`____ __ _ ___`
			`/ _/___/ /____(_)____ \|__ \`
[ rc ] For v0.6.9 - to see if the process was right Good luck everybody... v0.6.9 - Nice! ^^ 2023-11-30 15:48:46 +03:00			`/ // __ / ___/ / ___/ __/ / Version 0.6.9`
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> :exec main`
			`Enter a number: 6`
			`720`