Add redirect to index

src/Main.agda

@@ -3,11 +3,14 @@
 module main where
 
 open import Agda.Primitive renaming (Set to Type)
+
 import Data.String as S
 import Data.Vec as V
 import Data.List as L
 open S using (String)
 open L using (List)
+open V using (Vec)
+
 open import Data.Product using (_×_; proj₁; proj₂; _,_)
 open import Data.Nat hiding (_<_; _>_)
 open import Data.Unit using (⊤; tt)
@@ -146,6 +149,19 @@ module Pages where
 handle-request : HTTP.Request → IO Response
 handle-request req =
   case req .target .path of λ where
+    ($) →
+      pure (
+        record
+          { status-code = 302
+          ; status = "Found"
+          ; headers =
+            record
+              { name = ASCII.encode-list⁺ "Location"
+              ; value = ASCII.encode-list⁺ ("/" S.++ show ("index.html" / $))
+              } L.∷ L.[]
+          ; content = cake
+          }
+      )
     ("index.html" / $) →
       pure (
         200-ok text/html (HTML.Render.render-element (Pages.render-index (req .target .query)))