diff --git a/tests/lean/run/measurable.lean b/tests/lean/run/measurable.lean
deleted file mode 100644
index 42db77ff0e..0000000000
--- a/tests/lean/run/measurable.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-open prod nat
-
-example (a b : nat) : size_of (a, true, tt, (λ c d : nat, c + d), option.some b) = a + b :=
-rfl
-
-example : size_of (pair (pair (pair (2:nat) true) (λ a : nat, a)) (option.some (3:nat))) = 5 :=
-rfl