diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda
index 691fc4e7..bfc63a4a 100644
--- a/prototyping/Luau/OpSem.agda
+++ b/prototyping/Luau/OpSem.agda
@@ -5,7 +5,7 @@ open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; prim
 open import FFI.Data.Maybe using (just)
 open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
 open import Luau.Substitution using (_[_/_]ᴮ)
-open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; %; ^; number)
+open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; number)
 open import Luau.Value using (addr; val; number)
 
 evalBinOp : Float → BinaryOperator → Float → Float
@@ -13,8 +13,6 @@ evalBinOp x + y = primFloatPlus x y
 evalBinOp x - y = primFloatMinus x y
 evalBinOp x * y = primFloatTimes x y
 evalBinOp x / y = primFloatDiv x y
-evalBinOp x % y = x -- TODO: Actually implement this
-evalBinOp x ^ y = x -- TODO: Actually implement this
 
 data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
 data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set
diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda
index abd7e13e..c1c31e42 100644
--- a/prototyping/Luau/Syntax.agda
+++ b/prototyping/Luau/Syntax.agda
@@ -38,8 +38,6 @@ data BinaryOperator : Set where
   - : BinaryOperator
   * : BinaryOperator
   / : BinaryOperator
-  % : BinaryOperator
-  ^ : BinaryOperator
 
 data Block (a : Annotated) : Set
 data Stat (a : Annotated) : Set
diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda
index 1ebc9720..4a3061ba 100644
--- a/prototyping/Luau/Syntax/ToString.agda
+++ b/prototyping/Luau/Syntax/ToString.agda
@@ -1,7 +1,7 @@
 module Luau.Syntax.ToString where
 
 open import Agda.Builtin.Float using (primShowFloat)
-open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; binexp)
+open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; binexp)
 open import FFI.Data.String using (String; _++_)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Type.ToString using (typeToString)
@@ -18,12 +18,10 @@ funDecToString (f ⟨ x ⟩∈ T) = "function " ++ varToString f ++ "(" ++ varDe
 funDecToString (f ⟨ x ⟩) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ ")"
 
 binOpToString : BinaryOperator → String
-binOpToString BinaryOperator.+ = "+"
-binOpToString BinaryOperator.- = "-"
-binOpToString BinaryOperator.* = "*"
-binOpToString BinaryOperator./ = "/"
-binOpToString BinaryOperator.% = "%"
-binOpToString BinaryOperator.^ = "^"
+binOpToString + = "+"
+binOpToString - = "-"
+binOpToString * = "*"
+binOpToString / = "/"
 
 exprToString′ : ∀ {a} → String → Expr a → String
 statToString′ : ∀ {a} → String → Stat a → String