diff --git a/prototyping/Examples.agda b/prototyping/Examples.agda
new file mode 100644
index 00000000..4b576377
--- /dev/null
+++ b/prototyping/Examples.agda
@@ -0,0 +1,4 @@
+module Examples where
+
+import Examples.Syntax
+
diff --git a/prototyping/Examples/Syntax.agda b/prototyping/Examples/Syntax.agda
new file mode 100644
index 00000000..410ed505
--- /dev/null
+++ b/prototyping/Examples/Syntax.agda
@@ -0,0 +1,24 @@
+module Examples.Syntax where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import FFI.Data.String using (_++_)
+open import Luau.Syntax using (var; _$_; return; nil; function_⟨_⟩_end_)
+open import Luau.Syntax.ToString using (exprToString; blockToString)
+
+f = var "f"
+x = var "x"
+
+ex1 : exprToString(f $ x) ≡
+  "f(x)"
+ex1 = refl
+
+ex2 : blockToString(return nil) ≡
+  "return nil"
+ex2 = refl
+
+ex3 : blockToString(function "f" ⟨ "x" ⟩ return x end return f) ≡
+  "function f(x)\n" ++
+  "  return x\n" ++
+  "end\n" ++
+  "return f"
+ex3 = refl
diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda
index 8c1466fe..cc50ccde 100644
--- a/prototyping/Luau/Syntax/ToString.agda
+++ b/prototyping/Luau/Syntax/ToString.agda
@@ -13,6 +13,7 @@ blockToString′ : String → Block → String
 blockToString′ lb (function f ⟨ x ⟩ B end C) =
   "function " ++ f ++ "(" ++ x ++ ")" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
+  "end" ++ lb ++
   blockToString′ lb C
 blockToString′ lb (local x ← M ∙ B) =
   "local " ++ x ++ " = " ++ (exprToString M) ++ lb ++