From c600bca7472804b3ebe85aa4528dbd4eca3ed168 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 17 Dec 2017 21:47:05 +0100 Subject: [PATCH] feat(frontends/lean/definition_cmds): hide scary kernel exception on duplicate declaration --- src/frontends/lean/definition_cmds.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index b6849e38bc..ece3383e2d 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -249,6 +249,9 @@ declare_definition(parser & p, environment const & env, decl_cmd_kind kind, buff } else { c_real_name = get_namespace(env) + c_name; } + if (env.find(c_real_name)) { + throw exception(sstream() << "invalid definition, a declaration named '" << c_real_name << "' has already been declared"); + } if (val && !meta.m_modifiers.m_is_meta && !type_checker(env).is_prop(type)) { /* We only abstract nested proofs if the type of the definition is not a proposition */ std::tie(new_env, type) = abstract_nested_proofs(new_env, c_real_name, type);