From a009541b6ee091a6c4e3dadd72fc14f7dc1fdde2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 24 Nov 2016 14:51:45 -0800
Subject: [PATCH] test(tests/lean/run): add test for issue #1089

See #1089
---
 tests/lean/run/1089.lean | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 tests/lean/run/1089.lean

diff --git a/tests/lean/run/1089.lean b/tests/lean/run/1089.lean
new file mode 100644
index 0000000000..cede2af532
--- /dev/null
+++ b/tests/lean/run/1089.lean
@@ -0,0 +1,21 @@
+import init.string
+import init.bool
+import system.io
+
+inductive token
+| eof : token
+| plus : token
+| var : string -> token
+
+open token
+open option
+
+def to_token : string → option token
+| [] := none
+| (c :: cs) :=
+  let t : option token := match c with
+    | #"x" := some (var "x")
+    | #"y" := some (var "y")
+    | #"+" := some plus
+    | _ := none
+  end in t