From 65b962dabdfda8bb07fc713a4f5a34e533d92210 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Nov 2015 15:27:54 -0800
Subject: [PATCH] test(tests/lean/run): add basic tests for subst action

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

diff --git a/tests/lean/run/blast5.lean b/tests/lean/run/blast5.lean
new file mode 100644
index 0000000000..5886a3d9ee
--- /dev/null
+++ b/tests/lean/run/blast5.lean
@@ -0,0 +1,10 @@
+set_option blast.init_depth 10
+
+example (a b : nat) : a = b → b = a :=
+by blast
+
+example (a b c : nat) : a = b → a = c → b = c :=
+by blast
+
+example (p : nat → Prop) (a b c : nat) : a = b → a = c → p b → p c :=
+by blast