fix(frontends/lean): improve error message, addresses issue #299

src/frontends/lean/pp_options.cpp

@@ -93,13 +93,14 @@ void initialize_pp_options() {
                          "(pretty printer) apply beta-reduction when pretty printing");
 
     options universes_true(*g_pp_universes, true);
+    options full_names_true(*g_pp_full_names, true);
     options implicit_true(*g_pp_implicit, true);
     options coercions_true(*g_pp_coercions, true);
     options notation_false(*g_pp_notation, false);
     options implicit_coercions = join(coercions_true, implicit_true);
     options implicit_notation  = join(notation_false, implicit_true);
-    options all = join(join(universes_true, implicit_true), join(coercions_true, notation_false));
+    options all = universes_true + implicit_true + coercions_true + notation_false + full_names_true;
-    g_distinguishing_pp_options = new list<options>({implicit_true, coercions_true, implicit_coercions,
+    g_distinguishing_pp_options = new list<options>({implicit_true, full_names_true, coercions_true, implicit_coercions,
                 implicit_notation, universes_true, all});
 }
 

src/util/sexpr/options.h

@@ -85,6 +85,10 @@ inline options read_options(deserializer & d) { return options(read_sexpr(d)); }
 inline deserializer & operator>>(deserializer & d, options & o) { o = read_options(d); return d; }
 template<typename T> options update(options const & o, name const & n, T const & v) { return o.update(n, sexpr(v)); }
 
+inline options operator+(options const & opts1, options const & opts2) {
+    return join(opts1, opts2);
+}
+
 struct mk_option_declaration {
     mk_option_declaration(name const & n, option_kind k, char const * default_value, char const * description);
 };

tests/lean/error_full_names.lean

@@ -0,0 +1,10 @@
+import data.nat
+namespace foo
+open nat
+inductive nat : Type := zero, foosucc : nat → nat
+check 0 + nat.zero --error
+end foo
+
+namespace foo
+check nat.succ nat.zero --error
+end foo

tests/lean/error_full_names.lean.expected.out

@@ -0,0 +1,16 @@
+error_full_names.lean:5:8: error: type mismatch at application
+  0 + nat.zero
+term
+  nat.zero
+has type
+  nat
+but is expected to have type
+  ℕ
+error_full_names.lean:9:6: error: type mismatch at application
+  nat.succ nat.zero
+term
+  nat.zero
+has type
+  foo.nat
+but is expected to have type
+  nat