Example Chu2 Application in Agda ================================== ```agda module Hello where open import IO.Primitive using (IO; return) open import Foreign.Haskell using (Unit) open import Data.List using ([]) open import Chu2.ByteString using (pack) open import Function using (_$_; const) open import Chu2 postulate run : ApplicationData → IO Unit {-# IMPORT Chu2.Handler.SnapServerFFI #-} {-# COMPILED run Chu2.Handler.SnapServerFFI.run #-} hello-world-response = response OK [] (pack "Hello Agda!") hello-world-app : Application hello-world-app = const $ return hello-world-response main = run $ chu2 hello-world-app ``` Note ==== * need the Agda standard library: * need to read the Agda tutorial and be able to run Agda script from emacs: