Example Chu2 Application in Agda
module Hello where
import IO.Primitive as Prim
open import Chu2
open import Foreign.Haskell
open import Data.List
open import Chu2.ByteString
{-# IMPORT Chu2.Handler.SnapServerFFI #-}
postulate
runChu2 : Application -> Prim.IO Unit
{-# COMPILED runChu2 Chu2.Handler.SnapServerFFI.runChu2 #-}
hello_world_response = response OK [] (pack "Hello Agda!")
hello_world_app : Application
hello_world_app = \_ -> Prim.return hello_world_response
main = runChu2 hello_world_app
Note