diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index 12918f073e..e22069912d 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -318,6 +318,7 @@ environment add_alias(environment const & env, bool is_protected, name const & c
 
 struct definition_info {
     name     m_prefix;
+    bool     m_prev_errors{false};
     bool     m_is_private{false};
     bool     m_is_meta{false};
     bool     m_is_noncomputable{false};
@@ -328,11 +329,12 @@ struct definition_info {
 
 MK_THREAD_LOCAL_GET_DEF(definition_info, get_definition_info);
 
-declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, bool is_meta,
+declaration_info_scope::declaration_info_scope(name const & ns, bool prev_errors, bool is_private, bool is_meta,
                                                bool is_noncomputable, bool is_lemma, bool aux_lemmas) {
     definition_info & info = get_definition_info();
     lean_assert(info.m_prefix.is_anonymous());
-    info.m_prefix           = is_private ? name() : get_namespace(env);
+    info.m_prefix           = is_private ? name() : ns;
+    info.m_prev_errors      = prev_errors;
     info.m_is_private       = is_private;
     info.m_is_meta          = is_meta;
     info.m_is_noncomputable = is_noncomputable;
@@ -341,8 +343,8 @@ declaration_info_scope::declaration_info_scope(environment const & env, bool is_
     info.m_next_match_idx = 1;
 }
 
-declaration_info_scope::declaration_info_scope(environment const & env, bool is_private, bool is_noncomputable, def_cmd_kind k):
-    declaration_info_scope(env, is_private, k == MetaDefinition, is_noncomputable, k == Theorem, k == Definition) {}
+declaration_info_scope::declaration_info_scope(parser const & p, bool is_private, bool is_noncomputable, def_cmd_kind k):
+    declaration_info_scope(get_namespace(p.env()), p.found_errors(), is_private, k == MetaDefinition, is_noncomputable, k == Theorem, k == Definition) {}
 
 declaration_info_scope::~declaration_info_scope() {
     definition_info & info = get_definition_info();
@@ -358,6 +360,7 @@ equations_header mk_equations_header(list<name> const & ns) {
     h.m_is_noncomputable = get_definition_info().m_is_noncomputable;
     h.m_is_lemma         = get_definition_info().m_is_lemma;
     h.m_aux_lemmas       = get_definition_info().m_aux_lemmas;
+    h.m_prev_errors      = get_definition_info().m_prev_errors;
     return h;
 }
 
diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h
index 0caab61e9b..b2bc9b1414 100644
--- a/src/frontends/lean/decl_util.h
+++ b/src/frontends/lean/decl_util.h
@@ -82,9 +82,10 @@ environment add_alias(environment const & env, bool is_protected, name const & c
     This object is used to propagate relevant flags to
     nested definitions. */
 class declaration_info_scope {
+    declaration_info_scope(name const & ns, bool found_errors, bool is_private,
+                           bool is_meta, bool is_noncomputable, bool is_lemma, bool aux_lemmas);
 public:
-    declaration_info_scope(environment const & env, bool is_private, bool is_meta, bool is_noncomputable, bool is_lemma, bool aux_lemmas);
-    declaration_info_scope(environment const & env, bool is_private, bool is_noncomputable, def_cmd_kind k);
+    declaration_info_scope(parser const & p, bool is_private, bool is_noncomputable, def_cmd_kind k);
     ~declaration_info_scope();
 };
 
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 4947a708c8..a454bd6ccf 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/decl_attributes.h"
 #include "frontends/lean/definition_cmds.h"
+#include "frontends/lean/update_environment_exception.h"
 
 // We don't display profiling information for declarations that take less than 0.01 secs
 #ifndef LEAN_PROFILE_THRESHOLD
@@ -137,9 +138,8 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, bool is_pr
                                        decl_attributes /* attrs */) {
     buffer<name> lp_names;
     buffer<expr> fns, params;
-    declaration_info_scope scope(p.env(), is_private, is_noncomputable, kind);
+    declaration_info_scope scope(p, is_private, is_noncomputable, kind);
     expr val = parse_mutual_definition(p, lp_names, fns, params);
-    if (p.used_sorry()) p.declare_sorry();
     elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
     buffer<expr> new_params;
     elaborate_params(elab, params, new_params);
@@ -284,6 +284,8 @@ static environment compile_decl(parser & p, environment const & env, def_cmd_kin
         declaration d = env.get(c_real_name);
         return vm_compile(env, d);
     } catch (exception & ex) {
+        if (p.found_errors())
+            return env;
         flycheck_warning wrn(p.ios());
         auto & out = p.ios().get_regular_stream();
         display_pos(out, p, pos);
@@ -376,9 +378,8 @@ environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_private,
     buffer<expr> params;
     expr fn, val;
     auto header_pos = p.pos();
-    declaration_info_scope scope(p.env(), is_private, is_noncomputable, kind);
+    declaration_info_scope scope(p, is_private, is_noncomputable, kind);
     std::tie(fn, val) = parse_definition(p, lp_names, params, kind == def_cmd_kind::Example);
-    if (p.used_sorry()) p.declare_sorry();
     elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
     buffer<expr> new_params;
     elaborate_params(elab, params, new_params);
@@ -386,7 +387,17 @@ environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_private,
     replace_params(params, new_params, fn, val);
     bool is_meta = (kind == def_cmd_kind::MetaDefinition);
     expr type;
-    std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos);
+    std::shared_ptr<throwable> saved_exception;
+    try {
+        std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos);
+    } catch (exception & ex) {
+        if (kind == Example) throw;
+        /* Try again using 'sorry' */
+        saved_exception.reset(ex.clone());
+        val = p.mk_sorry(header_pos);
+        is_noncomputable = true;
+        std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos);
+    }
     if (is_meta) {
         val = fix_rec_fn_macro_args(elab, mlocal_name(fn), new_params, type, val);
     }
@@ -403,6 +414,9 @@ environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_private,
                                      is_meta, is_private, is_protected, is_noncomputable, attrs, header_pos);
     environment new_env = env_n.first;
     name c_real_name    = env_n.second;
-    return add_local_ref(p, new_env, c_name, c_real_name, lp_names, params);
+    new_env             = add_local_ref(p, new_env, c_name, c_real_name, lp_names, params);
+    if (saved_exception)
+        throw update_environment_exception(new_env, saved_exception);
+    return new_env;
 }
 }
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index f10d42e4bf..262a17970f 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/scope_pos_info_provider.h"
 #include "library/choice.h"
+#include "library/sorry.h"
 #include "library/util.h"
 #include "library/typed_expr.h"
 #include "library/annotation.h"
@@ -1264,6 +1265,10 @@ expr elaborator::visit_local(expr const & e, optional<expr> const & expected_typ
 }
 
 expr elaborator::visit_constant(expr const & e, optional<expr> const & expected_type) {
+    if (is_sorry(e)) {
+        m_env = declare_sorry(m_env);
+        m_ctx.set_env(m_env);
+    }
     return visit_app_core(e, buffer<expr>(), expected_type, e);
 }
 
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 63a153ce1c..ed3f9eb751 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -280,6 +280,7 @@ bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const
 
 expr parser::mk_sorry(pos_info const & p) {
     m_used_sorry = true;
+    m_ignore_noncomputable = true;
     {
 #ifndef LEAN_IGNORE_SORRY
         // TODO(Leo): remove the #ifdef.
@@ -293,11 +294,6 @@ expr parser::mk_sorry(pos_info const & p) {
     return save_pos(::lean::mk_sorry(), p);
 }
 
-void parser::declare_sorry() {
-    m_used_sorry = true;
-    m_env = ::lean::declare_sorry(m_env);
-}
-
 void parser::updt_options() {
     m_verbose        = get_verbose(m_ios.get_options());
     m_show_errors    = get_parser_show_errors(m_ios.get_options());
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index d6e8f3178b..9f21f09b15 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -224,6 +224,8 @@ public:
     bool ignore_noncomputable() const { return m_ignore_noncomputable; }
     void set_ignore_noncomputable() { m_ignore_noncomputable = true; }
 
+    bool found_errors() const { return m_found_errors; }
+
     name mk_anonymous_inst_name();
     bool is_anonymous_inst_name(name const & n) const;
 
@@ -484,7 +486,6 @@ public:
 
     expr mk_sorry(pos_info const & p);
     bool used_sorry() const { return m_used_sorry; }
-    void declare_sorry();
 
     void display_information_pos(pos_info p);
     void display_warning_pos(pos_info p);
diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp
index 6c3140f67e..df70febd01 100644
--- a/src/library/equations_compiler/elim_match.cpp
+++ b/src/library/equations_compiler/elim_match.cpp
@@ -1218,8 +1218,7 @@ expr mk_nonrec(environment & env, options const & opts, metavar_context & mctx,
     type_context ctx1(env, opts, mctx, lctx, transparency_mode::Semireducible);
     expr fn_type = ctx1.infer(R.m_fn);
     expr fn;
-    std::tie(env, fn) = mk_aux_definition(env, opts, mctx, lctx, header.m_is_private, header.m_is_lemma, header.m_is_noncomputable,
-                                          head(header.m_fn_names), fn_type, R.m_fn);
+    std::tie(env, fn) = mk_aux_definition(env, opts, mctx, lctx, header, head(header.m_fn_names), fn_type, R.m_fn);
     name fn_name = const_name(get_app_fn(fn));
     unsigned eqn_idx     = 1;
     type_context ctx2(env, opts, mctx, lctx, transparency_mode::Semireducible);
diff --git a/src/library/equations_compiler/equations.h b/src/library/equations_compiler/equations.h
index f74b88ec1a..ec80c709f2 100644
--- a/src/library/equations_compiler/equations.h
+++ b/src/library/equations_compiler/equations.h
@@ -34,6 +34,8 @@ struct equations_header {
     bool       m_is_meta{false};          /* the auxiliary declarations should be tagged as meta */
     bool       m_is_noncomputable{false}; /* if true, equation is not computable and code should not be generated */
     bool       m_aux_lemmas{false};       /* if true, we must create equation lemmas and induction principle */
+    bool       m_prev_errors{false};      /* if true, then errors have already being found processing the file,
+                                             and we should minimize error reporting */
     equations_header() {}
     equations_header(unsigned num_fns):m_num_fns(num_fns) {}
 };
diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp
index 98d5d2ec89..4da4add047 100644
--- a/src/library/equations_compiler/structural_rec.cpp
+++ b/src/library/equations_compiler/structural_rec.cpp
@@ -615,8 +615,8 @@ struct structural_rec_fn {
             return new_fn;
         } else {
             expr r;
-            std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, m_header.m_is_private, m_header.m_is_lemma,
-                                                   m_header.m_is_noncomputable, head(m_header.m_fn_names), m_fn_type, new_fn);
+            std::tie(m_env, r) = mk_aux_definition(m_env, m_opts, m_mctx, m_lctx, m_header,
+                                                   head(m_header.m_fn_names), m_fn_type, new_fn);
             return r;
         }
     }
diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp
index 51c80a7e63..583ba160cf 100644
--- a/src/library/equations_compiler/util.cpp
+++ b/src/library/equations_compiler/util.cpp
@@ -255,8 +255,7 @@ static void throw_mk_aux_definition_error(local_context const & lctx, name const
 }
 
 pair<environment, expr> mk_aux_definition(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
-                                          bool is_private, bool is_lemma, bool is_noncomputable,
-                                          name const & c, expr const & type, expr const & value) {
+                                          equations_header const & header, name const & c, expr const & type, expr const & value) {
     lean_trace("eqn_compiler", tout() << "declaring auxiliary definition\n" << c << " : " << type << "\n";);
     environment new_env = env;
     expr new_type       = type;
@@ -267,22 +266,24 @@ pair<environment, expr> mk_aux_definition(environment const & env, options const
         new_value = zeta_expand(lctx, new_value);
     }
     name new_c;
-    std::tie(new_env, new_c) = mk_def_name(env, is_private, c);
+    std::tie(new_env, new_c) = mk_def_name(env, header.m_is_private, c);
     expr r;
     try {
-        std::tie(new_env, r) = is_lemma ?
+        std::tie(new_env, r) = header.m_is_lemma ?
             mk_aux_lemma(new_env, mctx, lctx, new_c, new_type, new_value) :
             mk_aux_definition(new_env, mctx, lctx, new_c, new_type, new_value);
     } catch (exception & ex) {
         throw_mk_aux_definition_error(lctx, c, new_type, new_value, ex);
     }
-    if (!is_lemma && !is_noncomputable) {
+    if (!header.m_is_lemma && !header.m_is_noncomputable) {
         try {
             declaration d = new_env.get(new_c);
             new_env = vm_compile(new_env, d);
         } catch (exception & ex) {
-            throw nested_exception(sstream() << "equation compiler failed to generate bytecode for "
-                                   << "auxiliary declaration '" << c << "'", ex);
+            if (!header.m_prev_errors) {
+                throw nested_exception(sstream() << "equation compiler failed to generate bytecode for "
+                                       << "auxiliary declaration '" << c << "'", ex);
+            }
         }
     }
     return mk_pair(new_env, r);
diff --git a/src/library/equations_compiler/util.h b/src/library/equations_compiler/util.h
index 6c55ac098e..1fdef30f06 100644
--- a/src/library/equations_compiler/util.h
+++ b/src/library/equations_compiler/util.h
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "library/type_context.h"
+#include "library/equations_compiler/equations.h"
 namespace lean {
 [[ noreturn ]] void throw_ill_formed_eqns();
 
@@ -76,7 +77,7 @@ expr erase_inaccessible_annotations(expr const & e);
 list<expr> erase_inaccessible_annotations(list<expr> const & es);
 
 pair<environment, expr> mk_aux_definition(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
-                                          bool is_private, bool is_lemma, bool is_noncomputable, name const & n, expr const & type, expr const & value);
+                                          equations_header const & header, name const & n, expr const & type, expr const & value);
 
 environment mk_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
                               name const & f_name, unsigned eqn_idx, bool is_private,
diff --git a/tests/lean/minimize_errors.lean b/tests/lean/minimize_errors.lean
new file mode 100644
index 0000000000..d32b313c2b
--- /dev/null
+++ b/tests/lean/minimize_errors.lean
@@ -0,0 +1,16 @@
+def f : nat → nat → nat :=
+λ a, a
+
+check f
+
+def g : nat → nat → nat :=
+f
+
+check g
+
+print g
+
+def h : nat → nat → nat
+| x y := g x y + f y x
+
+print h
diff --git a/tests/lean/minimize_errors.lean.expected.out b/tests/lean/minimize_errors.lean.expected.out
new file mode 100644
index 0000000000..a7f8096659
--- /dev/null
+++ b/tests/lean/minimize_errors.lean.expected.out
@@ -0,0 +1,12 @@
+minimize_errors.lean:1:0: error: type mismatch, expression
+  λ (a : ℕ), a
+has type
+  ℕ → ℕ
+but is expected to have type
+  ℕ → ℕ → ℕ
+f : ℕ → ℕ → ℕ
+g : ℕ → ℕ → ℕ
+noncomputable definition g : ℕ → ℕ → ℕ :=
+f
+noncomputable definition h : ℕ → ℕ → ℕ :=
+h._main