[Bug 710383] Review Request: Agda - Commandline for dependently typed functional language

bugzilla at redhat.com bugzilla at redhat.com
Tue Jul 10 11:29:56 UTC 2012


https://bugzilla.redhat.com/show_bug.cgi?id=710383

--- Comment #3 from Shakthi Kannan <shakthimaan at gmail.com> ---
Even though the hackage page doesn't mention it, the Agda stdlib are required
for Agda-executable:

  http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.StandardLibrary

These need to be made available for use with the command line tool. For
example, in the following example the IO module is provided by the Agda stdlib:

=== TEST CODE ===

open import IO

main : _
main = run (putStrLn "Hello world!")

=== END ===

Gentoo (for example) has an ebuild for the same:

http://sources.gentoo.org/cgi-bin/viewvc.cgi/gentoo-x86/sci-mathematics/agda-stdlib/

-- 
You are receiving this mail because:
You are on the CC list for the bug.


More information about the haskell-devel mailing list