From a2e75159c85cdcbf2ef73f0133d7c1ebbf43410f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 2 Nov 2014 19:42:30 -0800
Subject: [PATCH] fix(frontends/lean): process choice-exprs at
 check_constant_next

---
 src/frontends/lean/parser.cpp    |  3 +++
 tests/lean/run/const_choice.lean | 12 ++++++++++++
 2 files changed, 15 insertions(+)
 create mode 100644 tests/lean/run/const_choice.lean

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 72573c181b..aeacf9d0c3 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1111,6 +1111,9 @@ name parser::check_constant_next(char const * msg) {
             e = get_explicit_arg(e);
     }
 
+    while (is_choice(e))
+        e = get_choice(e, 0);
+
     if (is_constant(e)) {
         return const_name(e);
     } else {
diff --git a/tests/lean/run/const_choice.lean b/tests/lean/run/const_choice.lean
new file mode 100644
index 0000000000..441421f9f0
--- /dev/null
+++ b/tests/lean/run/const_choice.lean
@@ -0,0 +1,12 @@
+import data.nat.basic
+open nat
+
+definition pred (a : nat) : nat :=
+nat.cases_on a
+  zero
+  (fun a₁, a₁)
+
+example : pred 1 = 0 :=
+rfl
+
+print definition pred