From 9ca065e7eebd402492ecc81ebd049ebf05e66834 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 23 Jul 2016 19:05:09 -0700
Subject: [PATCH] chore(tests/lean/run/measurable): remove obsolete test

---
 tests/lean/run/measurable.lean | 7 -------
 1 file changed, 7 deletions(-)
 delete mode 100644 tests/lean/run/measurable.lean

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