diff --git a/C0deine/Utils/Comparison.lean b/C0deine/Utils/Comparison.lean
index 56b4e1f..1a6c7ef 100644
--- a/C0deine/Utils/Comparison.lean
+++ b/C0deine/Utils/Comparison.lean
@@ -2,6 +2,7 @@
    Basic comparison operators that are used in numerous IRs.
    - Thea Brick
  -/
+import Lean
 namespace C0deine
 
 inductive Comparator
@@ -27,3 +28,16 @@ def toString : Comparator → String
   | less_equal => "<="
   | greater_equal => ">="
 instance : ToString Comparator where toString := Comparator.toString
+
+instance : Lean.ToExpr Comparator :=
+{
+  toExpr := fun c =>
+    match c with
+    | Comparator.less    => Lean.mkConst ``Comparator.less
+    | Comparator.equal   => Lean.mkConst ``Comparator.equal
+    | Comparator.greater => Lean.mkConst ``Comparator.greater
+    | Comparator.not_equal => Lean.mkConst ``Comparator.not_equal
+    | Comparator.less_equal => Lean.mkConst ``Comparator.less_equal
+    | Comparator.greater_equal => Lean.mkConst ``Comparator.greater_equal
+  toTypeExpr := Lean.mkConst ``Comparator
+}