From 9812cfe906b199406dc314fbcdc588c94d0f67bc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 9 May 2015 12:02:52 -0700
Subject: [PATCH] test(tests/lean/run): add example for constructive choice

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

diff --git a/tests/lean/run/choose_test.lean b/tests/lean/run/choose_test.lean
new file mode 100644
index 0000000000..171b870b9d
--- /dev/null
+++ b/tests/lean/run/choose_test.lean
@@ -0,0 +1,12 @@
+import data.encodable
+open nat encodable
+
+theorem ex : ∃ x, x > 3 :=
+exists.intro 6 dec_trivial
+
+reveal ex
+
+eval choose ex
+
+example : choose ex = 4 :=
+rfl