1 files changed, 0 insertions, 35 deletions
diff --git a/src/Compilers/TypeUtil.v b/src/Compilers/TypeUtil.v
deleted file mode 100644
index 050374562..000000000
--- a/src/Compilers/TypeUtil.v
+++ /dev/null
@@ -1,35 +0,0 @@
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Util.Notations.
-
-Local Open Scope expr_scope.
-
-Section language.
-  Context {base_type_code : Type}
-          (base_type_beq : base_type_code -> base_type_code -> bool)
-          (base_type_leb : base_type_code -> base_type_code -> bool).
-  Local Infix "<=?" := base_type_leb : expr_scope.
-  Local Infix "=?" := base_type_beq : expr_scope.
-
-  Definition base_type_min (a b : base_type_code) : base_type_code
-    := if a <=? b then a else b.
-  Definition base_type_max (a b : base_type_code) : base_type_code
-    := if a <=? b then b else a.
-  Section gen.
-    Context (join : base_type_code -> base_type_code -> base_type_code).
-    Fixpoint flat_type_join {t : flat_type base_type_code}
-      : interp_flat_type (fun _ => base_type_code) t -> option base_type_code
-      := match t with
-         | Tbase _ => fun v => Some v
-         | Unit => fun _ => None
-         | Prod A B
-           => fun v => match @flat_type_join A (fst v), @flat_type_join B (snd v) with
-                       | Some a, Some b => Some (join a b)
-                       | Some a, None => Some a
-                       | None, Some b => Some b
-                       | None, None => None
-                       end
-         end.
-  End gen.
-  Definition flat_type_min {t} := @flat_type_join base_type_min t.
-  Definition flat_type_max {t} := @flat_type_join base_type_max t.
-End language.