From f4fd0ca77551833243baf122034cde760d5c75ef Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 22 Aug 2016 13:30:37 -0700
Subject: [PATCH] fix(frontends/lean/definition_cmds): empty set of equations

---
 src/frontends/lean/definition_cmds.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index af6add5efc..47f33abce3 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -144,7 +144,7 @@ expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & p
     if (p.curr_is_token(get_assign_tk())) {
         p.next();
         val = p.parse_expr();
-    } else if (p.curr_is_token(get_bar_tk())) {
+    } else if (p.curr_is_token(get_bar_tk()) || p.curr_is_token(get_none_tk())) {
         p.add_local(fn);
         buffer<expr> eqns;
         if (p.curr_is_token(get_none_tk())) {