Agda 2

Примеры:

Hello, World!:

Простой вывод строк на печать — неестественное для Agda занятие, поэтому требует установки дополнительных пакетов. Этот пример следует сохранить в файл “helloworld.agda”. Понадобится установить стандартную библиотеку agda-stdlib; этот пример был проверен для agda 2.2.6 и agda-stdlib 0.3. Чтобы скомпилировать пример, используйте команду agda -i [library path] -i . -c helloworld.agda, где [library path] — путь к директории, в которой установлена библиотека. Эта команда компилирует исходный код Agda в код Haskell, и затем — в исполняемый файл.

module helloworld where

open import IO.Primitive using (IO; putStrLn)
open import Data.String using (toCostring; String)
open import Data.Char using (Char)
open import Foreign.Haskell using (fromColist; Colist; Unit)
open import Data.Function

fromString = fromColist . toCostring

main : IO Unit
main = putStrLn (fromString "Hello, World!")