[Agda] how to run helloworld in agda

[Andrés Sicard-Ramírez]

On 20 December 2015 at 02:16, Mandy Martino <tesleft at hotmail.com> wrote:
> got  error  No binding for builtin thing IO, use {-# BUILTIN IO name #-} to
> bind it to 'name'

I suggest first understand the translation from Agda into GHC without
using the standard library. I attached a simple example compatible
with Agda 2.4.2.5.

There is some documentation on compiling Agda programs in Section 4 of

  http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

whose source code (not fully compatible with Agda 2.4.2.5) is in

  http://www.cse.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/


-- 
Andrés
-------------- next part --------------
A non-text attachment was scrubbed...
Name: HelloWorld.agda
Type: application/octet-stream
Size: 645 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20151220/36f4b815/HelloWorld.obj