WIP

README.md

@@ -68,6 +68,8 @@ rm -rf /usr/local/share/emacs/site-lisp/agda
 Save the following code into a file called `hello.agda`.
 
 ```agda
+{-# OPTIONS --guardedness #-}
+
 open import Prelude
 open import System.IO
 
@@ -85,38 +87,7 @@ agda --compile hello.agda
 
 Save the following code into a file called `echo-server.agda`:
 
-```agda
-{-# OPTIONS --guardedness #-}
-
-open import Prelude
-
-open import Data.Bytes as Bytes using ()
-open import Data.List as List using ()
-open import Data.String.Encoding
-open import Network.Socket
-open import System.IO
-
-runTCPEchoServer : IO Unit
-runTCPEchoServer = do
-  (serverAddr , _) <- getAddrInfo nothing (just "127.0.0.1") (just "7000")
-  serverSocket <- socket (addrFamily serverAddr) sockStream defaultProtocol
-  setSocketOption serverSocket reuseAddr 1
-  bind serverSocket (addrAddress serverAddr)
-  listen serverSocket 1
-  (clientSocket , _) <- accept serverSocket
-  print {String} "Waiting for a message..."
-  message <- recv clientSocket 1024
-  unless (Bytes.null message) do
-    print ("Received: " <> decodeUtf8 message)
-    print {String} "Echoing..."
-    sendAll clientSocket message
-  print {String} "Closing..."
-  close clientSocket
-  close serverSocket
-
-main : IO Unit
-main = runTCPEchoServer
-```
+https://github.com/berndlosert/agda-base/blob/master/examples/echo-server.agda#L1-L30
 
 Compile this code by running `agda --compile echo-server.agda`. If you get the
 following errors:

examples/echo-server.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 open import Prelude
 
 open import Data.Bytes as Bytes using ()