<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>is there an example to use function in Algebra folder</div><div>and import Algebra?</div><div><br></div><div> i would like to test what is the correct command to compile example for std-lib .</div><div><br><div>Regards,</div><div><br></div><div>Martin </div><br><br><div>> From: asr@eafit.edu.co<br>> Date: Sat, 19 Dec 2015 05:04:14 -0500<br>> Subject: Re: [Agda] how to run helloworld in agda<br>> To: tesleft@hotmail.com<br>> CC: leo@halfaya.org; ulf.norell@gmail.com; agda@lists.chalmers.se<br>> <br>> On 19 December 2015 at 03:40, Mandy Martino <tesleft@hotmail.com> wrote:<br>> > time agda -c hello.agda -i. -iagda-prelude/src -iagda-stdlib/src<br>> > --ghc-flag=agda-prelude/agda-ffi/Agda/FFI.hs<br>> ><br>> > got error when run above command, would like to display some simple<br>> > result when using Algebra library in stdlibrary,<br>> <br>> By removing `-iagda-stdlib/src` in the above command, you can run the<br>> hello program:<br>> <br>> $ time agda -c hello.agda -i. -iagda-prelude/src<br>> --ghc-flag=agda-prelude/agda-ffi/Agda/FFI.hs<br>> $ ./hello<br>> Hello World<br>> <br>> -- <br>> Andrés<br></div></div> </div></body>
</html>