diff --git a/spectec/doc/Language.md b/spectec/doc/Language.md
index f8cfd761fe..ea739d04e4 100644
--- a/spectec/doc/Language.md
+++ b/spectec/doc/Language.md
@@ -154,7 +154,7 @@ exp ::=
   "##" exp                             remove possible parentheses (for syntax rewrites in hints)
 
 unop  ::= notop | "+" | "-"
-binop ::= logop | "+" | "-" | "*" | "/" | "^"
+binop ::= logop | "+" | "-" | "*" | "/" | "\" | "^"
 arith ::=
   varid                                meta variable
   atom                                 token
diff --git a/spectec/src/al/ast.ml b/spectec/src/al/ast.ml
index 7fb553814e..f0d657e4cc 100644
--- a/spectec/src/al/ast.ml
+++ b/spectec/src/al/ast.ml
@@ -49,6 +49,7 @@ type binop =
   | SubOp    (* `-` *)
   | MulOp    (* `*` *)
   | DivOp    (* `/` *)
+  | ModOp    (* `\` *)
   | ExpOp    (* `^` *)
   (* logical operation *)
   | ImplOp   (* `=>` *)
diff --git a/spectec/src/al/print.ml b/spectec/src/al/print.ml
index ad73ff6afe..5f7a7920fa 100644
--- a/spectec/src/al/print.ml
+++ b/spectec/src/al/print.ml
@@ -91,6 +91,7 @@ let string_of_binop = function
   | SubOp -> "-"
   | MulOp -> "·"
   | DivOp -> "/"
+  | ModOp -> "\\"
   | ExpOp -> "^"
   | EqOp -> "is"
   | NeOp -> "is not"
diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml
index d6575500a0..770e5adbdb 100644
--- a/spectec/src/backend-interpreter/interpreter.ml
+++ b/spectec/src/backend-interpreter/interpreter.ml
@@ -136,6 +136,7 @@ and eval_expr env expr =
     | SubOp, NumV i1, NumV i2 -> Z.sub i1 i2 |> numV
     | MulOp, NumV i1, NumV i2 -> Z.mul i1 i2 |> numV
     | DivOp, NumV i1, NumV i2 -> Z.div i1 i2 |> numV
+    | ModOp, NumV i1, NumV i2 -> Z.rem i1 i2 |> numV
     | ExpOp, NumV i1, NumV i2 -> Z.pow i1 (Z.to_int i2) |> numV
     | AndOp, BoolV b1, BoolV b2 -> boolV (b1 && b2)
     | OrOp, BoolV b1, BoolV b2 -> boolV (b1 || b2)
diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml
index daa3c0112d..3ebc907f8f 100644
--- a/spectec/src/backend-latex/render.ml
+++ b/spectec/src/backend-latex/render.ml
@@ -830,6 +830,7 @@ let render_binop = function
   | SubOp -> "-"
   | MulOp -> "\\cdot"
   | DivOp -> "/"
+  | ModOp -> "\\mathbin{mod}"
   | ExpOp -> assert false
 
 let render_cmpop = function
diff --git a/spectec/src/backend-prose/render.ml b/spectec/src/backend-prose/render.ml
index 3f4f78aac0..2d5060874b 100644
--- a/spectec/src/backend-prose/render.ml
+++ b/spectec/src/backend-prose/render.ml
@@ -44,6 +44,7 @@ let al_to_el_binop = function
   | Al.Ast.SubOp -> Some El.Ast.SubOp
   | Al.Ast.MulOp -> Some El.Ast.MulOp
   | Al.Ast.DivOp -> Some El.Ast.DivOp
+  | Al.Ast.ModOp -> Some El.Ast.ModOp
   | Al.Ast.ExpOp -> Some El.Ast.ExpOp
   | _ -> None
 
@@ -247,6 +248,7 @@ let render_al_binop = function
   | Al.Ast.SubOp -> "minus"
   | Al.Ast.MulOp -> "multiplied by"
   | Al.Ast.DivOp -> "divided by"
+  | Al.Ast.ModOp -> "modulo"
   | Al.Ast.ExpOp -> "to the power of"
   | Al.Ast.EqOp -> "is"
   | Al.Ast.NeOp -> "is not"
diff --git a/spectec/src/el/ast.ml b/spectec/src/el/ast.ml
index 3c9f771900..233c607f47 100644
--- a/spectec/src/el/ast.ml
+++ b/spectec/src/el/ast.ml
@@ -86,6 +86,7 @@ and binop =
   | SubOp  (* `-` *)
   | MulOp  (* `*` *)
   | DivOp  (* `/` *)
+  | ModOp  (* `\` *)
   | ExpOp  (* `^` *)
 
 and cmpop =
diff --git a/spectec/src/el/print.ml b/spectec/src/el/print.ml
index e2fbd3e643..7b6529923a 100644
--- a/spectec/src/el/print.ml
+++ b/spectec/src/el/print.ml
@@ -41,6 +41,7 @@ let string_of_binop = function
   | SubOp -> "-"
   | MulOp -> "*"
   | DivOp -> "/"
+  | ModOp -> "\\"
   | ExpOp -> "^"
 
 let string_of_cmpop = function
diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml
index ff7672392d..48193d981b 100644
--- a/spectec/src/frontend/elab.ml
+++ b/spectec/src/frontend/elab.ml
@@ -511,6 +511,7 @@ let infer_binop' = function
   | SubOp -> infer_numop (fun t -> Il.SubOp t) numtyps
   | MulOp -> infer_numop (fun t -> Il.MulOp t) numtyps
   | DivOp -> infer_numop (fun t -> Il.DivOp t) numtyps
+  | ModOp -> infer_numop (fun t -> Il.ModOp t) numtyps
   | ExpOp -> infer_numop (fun t -> Il.ExpOp t) numtyps
 
 let infer_cmpop' = function
diff --git a/spectec/src/frontend/eval.ml b/spectec/src/frontend/eval.ml
index f29bbd82b8..71bd70484a 100644
--- a/spectec/src/frontend/eval.ml
+++ b/spectec/src/frontend/eval.ml
@@ -174,6 +174,9 @@ and reduce_exp env e : exp =
     | DivOp, NatE (op, n1), NatE (_, n2) -> NatE (op, Z.(n1 / n2)) $ e.at
     | DivOp, NatE (_, z0), _ when z0 = Z.zero -> e1'
     | DivOp, _, NatE (_, z1) when z1 = Z.one -> e1'
+    | ModOp, NatE (op, n1), NatE (_, n2) -> NatE (op, Z.rem n1 n2) $ e.at
+    | ModOp, NatE (_, z0), _ when z0 = Z.zero -> e1'
+    | ModOp, _, NatE (op, z1) when z1 = Z.one -> NatE (op, Z.zero) $ e.at
     | ExpOp, NatE (op, n1), NatE (_, n2) -> NatE (op, Z.(n1 ** to_int n2)) $ e.at
     | ExpOp, NatE (_, z01), _ when z01 = Z.zero || z01 = Z.one -> e1'
     | ExpOp, _, NatE (op, z0) when z0 = Z.zero -> NatE (op, Z.one) $ e.at
diff --git a/spectec/src/frontend/parser.mly b/spectec/src/frontend/parser.mly
index 84d39c7822..fe9615196f 100644
--- a/spectec/src/frontend/parser.mly
+++ b/spectec/src/frontend/parser.mly
@@ -293,6 +293,7 @@ check_atom :
   | MINUS { SubOp }
   | STAR { MulOp }
   | SLASH { DivOp }
+  | BACKSLASH { ModOp }
 
 %inline cmpop :
   | EQ { EqOp }
diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml
index 88c3d5003f..1d7720d001 100644
--- a/spectec/src/il/ast.ml
+++ b/spectec/src/il/ast.ml
@@ -67,6 +67,7 @@ and binop =
   | SubOp of numtyp  (* `-` *)
   | MulOp of numtyp  (* `*` *)
   | DivOp of numtyp  (* `/` *)
+  | ModOp of numtyp  (* `\` *)
   | ExpOp of numtyp  (* `^` *)
 
 and cmpop =
diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml
index 92eef52474..9bc378e4ea 100644
--- a/spectec/src/il/eval.ml
+++ b/spectec/src/il/eval.ml
@@ -160,6 +160,9 @@ and reduce_exp env e : exp =
     | DivOp _, NatE n1, NatE n2 -> NatE Z.(n1 / n2) $> e
     | DivOp _, NatE z0, _ when z0 = Z.zero -> e1'
     | DivOp _, _, NatE z1 when z1 = Z.one -> e1'
+    | ModOp _, NatE n1, NatE n2 -> NatE Z.(rem n1 n2) $> e
+    | ModOp _, NatE z0, _ when z0 = Z.zero -> e1'
+    | ModOp _, _, NatE z1 when z1 = Z.one -> NatE Z.zero $> e
     | ExpOp _, NatE n1, NatE n2 -> NatE Z.(n1 ** to_int n2) $> e
     | ExpOp _, NatE z01, _ when z01 = Z.zero || z01 = Z.one -> e1'
     | ExpOp _, _, NatE z0 when z0 = Z.zero -> NatE Z.one $> e
diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml
index 062b8962cf..7f5a479b21 100644
--- a/spectec/src/il/print.ml
+++ b/spectec/src/il/print.ml
@@ -28,6 +28,7 @@ let string_of_binop = function
   | SubOp _ -> "-"
   | MulOp _ -> "*"
   | DivOp _ -> "/"
+  | ModOp _ -> "\\"
   | ExpOp _ -> "^"
 
 let string_of_cmpop = function
diff --git a/spectec/src/il/valid.ml b/spectec/src/il/valid.ml
index 45ba90c446..8fac3f1483 100644
--- a/spectec/src/il/valid.ml
+++ b/spectec/src/il/valid.ml
@@ -149,7 +149,7 @@ let infer_unop = function
 
 let infer_binop = function
   | AndOp | OrOp | ImplOp | EquivOp -> BoolT, BoolT, BoolT
-  | AddOp t | SubOp t | MulOp t | DivOp t -> NumT t, NumT t, NumT t
+  | AddOp t | SubOp t | MulOp t | DivOp t | ModOp t -> NumT t, NumT t, NumT t
   | ExpOp t -> NumT t, NumT NatT, NumT t
 
 let infer_cmpop = function
diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml
index bb4d28ccb8..469de4dd1a 100644
--- a/spectec/src/il2al/translate.ml
+++ b/spectec/src/il2al/translate.ml
@@ -159,6 +159,7 @@ and translate_exp exp =
       | Il.SubOp _ -> SubOp
       | Il.MulOp _ -> MulOp
       | Il.DivOp _ -> DivOp
+      | Il.ModOp _ -> ModOp
       | Il.ExpOp _ -> ExpOp
       | Il.AndOp -> AndOp
       | Il.OrOp -> OrOp