From a4e72e526264854e6b214f168038d86816cbef5d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 May 2015 17:02:23 -0700
Subject: [PATCH] test(tests/lean/run): add missing test

---
 tests/lean/run/subst_test2.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 tests/lean/run/subst_test2.lean

diff --git a/tests/lean/run/subst_test2.lean b/tests/lean/run/subst_test2.lean
new file mode 100644
index 000000000..1f4e55088
--- /dev/null
+++ b/tests/lean/run/subst_test2.lean
@@ -0,0 +1,17 @@
+import data.nat
+open nat
+
+structure less_than (n : nat) := (val : nat) (lt : val < n)
+
+namespace less_than
+open decidable
+
+set_option pp.beta false
+
+definition less_than.has_decidable_eq [instance] (n : nat) : ∀ (i j : less_than n), decidable (i = j)
+| (mk ival ilt) (mk jval jlt) :=
+  match nat.has_decidable_eq ival jval with
+  | inl veq := inl (by substvars)
+  | inr vne := inr (by intro h; injection h; contradiction)
+  end
+end less_than