agda で "Hello, world!" - x76789の研究メモAgda で入出力を扱う場合，Agda の FFI（Foreign Function Interface）を通し，Haskellの入出力関数を用いておこなう． 実際に，「Hello, World」プログラムをAgdaで作成してみた．ちなみに，入出力をおこなうには，コンパイルしておこなう必要がある．詳細は以下の通り． hello.agda module hello where data Unit : Set where unit : Unit {-# COMPILED_DATA Unit () () #-} data List (A : Set) : Set where [] : List A _::_ : A -> List A -> List A {-# BUILTIN LIST List #-} {-# BUILTIN NIL [] #-} {-# BUILTIN CONS _::_
