From 7cdec2c8f35242ea71b2b79c12b777038353f8b1 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Fri, 7 Oct 2016 13:30:52 -0700
Subject: [PATCH] chore(frontents/lean/definition_cmds): improve error message

---
 src/frontends/lean/definition_cmds.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 1c4773f841..e49500ec7c 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -122,6 +122,9 @@ expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<expr> &
             while (p.curr_is_token(get_bar_tk())) {
                 eqns.push_back(parse_equation(p, pre_fn));
             }
+            if (!p.curr_is_command() && !p.curr_is_eof()) {
+                throw parser_error("invalid equations, must be followed by a command or EOF", p.pos());
+            }
         }
         expr fn      = mk_local(mlocal_name(pre_fn), local_pp_name(pre_fn), fn_type, mk_rec_info(true));
         fns.push_back(fn);
@@ -177,6 +180,9 @@ static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<ex
             while (p.curr_is_token(get_bar_tk())) {
                 eqns.push_back(parse_equation(p, fn));
             }
+            if (!p.curr_is_command() && !p.curr_is_eof()) {
+                throw parser_error("invalid equations, must be followed by a command or EOF", p.pos());
+            }
         }
         optional<expr_pair> R_Rwf = parse_using_well_founded(p);
         val = mk_equations(p, fn, scope2.get_name(), eqns, R_Rwf, header_pos);