diff --git a/prototyping/Examples/Syntax.agda b/prototyping/Examples/Syntax.agda
index 73160ca0..4ffcf4c5 100644
--- a/prototyping/Examples/Syntax.agda
+++ b/prototyping/Examples/Syntax.agda
@@ -6,7 +6,7 @@ open import Luau.Syntax using (var; _$_; return; nil; function_is_end; local_←
 open import Luau.Syntax.ToString using (exprToString; blockToString)
 
 ex1 : exprToString(function "" ⟨ var "x" ⟩ is return (var "f" $ var "x") ∙ done end) ≡
-  "function (x)\n" ++
+  "function(x)\n" ++
   "  return f(x)\n" ++
   "end"
 ex1 = refl
diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda
index 8ab5eece..18d36175 100644
--- a/prototyping/Luau/Syntax/ToString.agda
+++ b/prototyping/Luau/Syntax/ToString.agda
@@ -11,8 +11,10 @@ varDecToString (var x) = varToString x
 varDecToString (var x ∈ T) =  varToString x ++ " : " ++ typeToString T
 
 funDecToString : ∀ {a} → FunDec a → String
-funDecToString (f ⟨ x ⟩∈ T) = varToString f ++ "(" ++ varDecToString x ++ "): " ++ typeToString T
-funDecToString (f ⟨ x ⟩) = varToString f ++ "(" ++ varDecToString x ++ ")"
+funDecToString ("" ⟨ x ⟩∈ T) = "function(" ++ varDecToString x ++ "): " ++ typeToString T
+funDecToString ("" ⟨ x ⟩) = "function(" ++ varDecToString x ++ ")"
+funDecToString (f ⟨ x ⟩∈ T) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ "): " ++ typeToString T
+funDecToString (f ⟨ x ⟩) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ ")"
 
 exprToString′ : ∀ {a} → String → Expr a → String
 statToString′ : ∀ {a} → String → Stat a → String
@@ -27,16 +29,16 @@ exprToString′ lb (var x) =
 exprToString′ lb (M $ N) =
   (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")"
 exprToString′ lb (function F is B end) =
-  "function " ++ funDecToString F ++ lb ++
+  funDecToString F ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end"
 exprToString′ lb (block b is B end) =
-  "(function " ++ b ++ "()" ++ lb ++
+  "(" ++ b ++ "()" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end)()"
 
 statToString′ lb (function F is B end) =
-  "local function " ++ funDecToString F ++ lb ++
+  "local " ++ funDecToString F ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end"
 statToString′ lb (local x ← M) =