fix(frontends/lean): wrong displayed type in proof with multiple sorry's, fixes #112

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/parser.cpp

@@ -148,7 +148,7 @@ expr parser::mk_sorry(pos_info const & p) {
         display_warning_pos(p.first, p.second);
         regular_stream() << " using 'sorry'" << endl;
     }
-    return get_sorry_constant();
+    return save_pos(::lean::mk_sorry(), p);
 }
 
 void parser::declare_sorry() {

src/library/sorry.cpp

@@ -10,7 +10,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name g_sorry_name("sorry");
-static expr g_sorry(mk_constant(g_sorry_name));
 static name  g_l("l");
 static expr  g_sorry_type(mk_pi("A", mk_sort(mk_param_univ(g_l)), mk_var(0), binder_info(true)));
 
@@ -29,6 +28,6 @@ environment declare_sorry(environment const & env) {
     }
 }
 
-expr const & get_sorry_constant() { return g_sorry; }
+expr mk_sorry() { return mk_constant(g_sorry_name); }
 name const & get_sorry_name() { return g_sorry_name; }
 }

src/library/sorry.h

@@ -16,6 +16,6 @@ bool has_sorry(environment const & env);
 environment declare_sorry(environment const & env);
 
 /** \brief Return the constant \c sorry */
-expr const & get_sorry_constant();
+expr mk_sorry();
 name const & get_sorry_name();
 }

tests/lean/interactive/in5.input

@@ -0,0 +1,3 @@
+VISIT sorry2.lean
+WAIT
+INFO 4

tests/lean/interactive/in5.input.expected.out

@@ -0,0 +1,20 @@
+-- BEGININFO
+-- TYPE|4|0
+A → B → and A B
+-- ACK
+-- IDENTIFIER|4|0
+and_intro
+-- ACK
+-- TYPE|4|10
+A
+-- ACK
+-- SYMBOL|4|10
+sorry
+-- ACK
+-- TYPE|4|16
+B
+-- ACK
+-- SYMBOL|4|16
+sorry
+-- ACK
+-- ENDINFO

tests/lean/interactive/sorry2.lean

@@ -0,0 +1,4 @@
+import logic
+
+theorem tst (A B : Prop) : A ∧ B :=
+and_intro sorry sorry