<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:新細明體
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><font size="3" style="font-size:12pt;" color="#000000">Hi Andres,</font><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div>got error <span style="font-size: 12pt;">No binding for builtin thing IO, use {-# BUILTIN IO name #-} to</span></div><div>bind it to 'name'</div><div><br></div><div>even if no main :: IO Unit</div><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font color="#000000"><div>Compiling hello in /home/martin/hilbertreborn/hello.agdai to /home/martin/hilbertreborn/MAlonzo/Code/Qhello.hs</div><div>No binding for builtin thing IO, use {-# BUILTIN IO name #-} to</div><div>bind it to 'name'</div><div><br></div><div>real<span class="Apple-tab-span" style="white-space:pre"> </span>0m4.174s</div><div>user<span class="Apple-tab-span" style="white-space:pre"> </span>0m1.348s</div><div>sys<span class="Apple-tab-span" style="white-space:pre"> </span>0m1.492s</div><div>martin@ubuntu:~/hilbertreborn$ cat hello.agda</div><div>module hello where</div><div>open import Data.Nat.Base</div><div>open import Relation.Binary.PropositionalEquality</div><div>open import Algebra.Structures as A using (IsCommutativeMonoid)</div><div>open import Data.Nat.Properties using (isCommutativeSemiring)</div><div><br></div><div>open A.IsCommutativeSemiring</div><div>open A.IsCommutativeMonoid (+-isCommutativeMonoid isCommutativeSemiring)</div><div><br></div><div>ex : ∀ n → (n + 1) + 1 ≡ n + 2</div><div>ex n = assoc n 1 1</div><div><br></div><div>main = ex</div><div style="font-size: 12pt;"><br></div></font><br><br><div>Regards,</div><div><br></div><div>Martin </div><br><br><div>> From: asr@eafit.edu.co<br>> Date: Sat, 19 Dec 2015 13:08:18 -0500<br>> Subject: Re: [Agda] how to run helloworld in agda<br>> To: tesleft@hotmail.com<br>> CC: agda@lists.chalmers.se<br>> <br>> On 19 December 2015 at 08:06, Mandy Martino <tesleft@hotmail.com> wrote:<br>> > After meet message need {-# BUILTIN IO name #-},<br>> ><br>> > i add {-# BUILTIN IO name #-} or {-# BUILTIN IO hello #-}, still have<br>> > error,<br>> ><br>> > when and where need this?<br>> <br>> See http://agda.readthedocs.org/en/latest/language/built-ins.html#io .<br>> <br>> You can use the IO from the standard library as I showed in an previous example.<br>> <br>> > ex : ∀ n → (n + 1) + 1 ≡ n + 2<br>> > ex n = assoc n 1 1<br>> ><br>> > main : IO Unit<br>> > main = ex<br>> <br>> Since `ex` hasn't type `IO Unit` you'll get a type error.<br>> <br>> <br>> -- <br>> Andrés<br></div></div> </div></body>
</html>