feat(frontends/lean): try overloaded notation and declarations in the order they were defined

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

src/frontends/lean/elaborator.cpp

@@ -368,15 +368,15 @@ class elaborator {
                                list<expr> const & ctx, list<expr> const & full_ctx,
                                bool relax):
             m_elab(elab), m_mvar(mvar), m_choice(c), m_ctx(ctx), m_full_ctx(full_ctx),
-            m_idx(0), m_relax_main_opaque(relax) {
+            m_idx(get_num_choices(m_choice)), m_relax_main_opaque(relax) {
         }
 
         virtual optional<constraints> next() {
-            while (m_idx < get_num_choices(m_choice)) {
+            while (m_idx > 0) {
+                --m_idx;
                 expr const & c = get_choice(m_choice, m_idx);
                 expr const & f = get_app_fn(c);
                 m_elab.save_identifier_info(f);
-                m_idx++;
                 try {
                     new_scope s(m_elab, m_ctx, m_full_ctx);
                     expr r = m_elab.visit(c);

tests/lean/run/alias1.lean

@@ -30,15 +30,16 @@ check foo a b
 theorem T1 : foo a b = N1.foo a b
 := refl _
 
-definition aux1 := foo a b  -- System elaborated it to N2.foo (f a) (f b)
+definition aux1 := foo a b  -- System elaborated it to N1.foo a b
-theorem T2 : aux1 = N2.foo (f a) (f b)
+#erase_cache T2
+theorem T2 : aux1 = N1.foo a b
 := refl _
 
 using N1
-definition aux2 := foo a b  -- Now N1 is in the beginning of the queue again, and this is elaborated to N1.foo a b
+definition aux2 := foo a b  -- Now N1 is in the end of the queue, this is elaborated to N2.foo (f a) (f b)
 check aux2
 
-theorem T3 : aux2 = N1.foo a b
+theorem T3 : aux2 = N2.foo (f a) (f b)
 := refl aux2
 
 

tests/lean/run/alias2.lean

@@ -10,8 +10,8 @@ namespace N2
   variable foo : val → val → val
 end N2
 
-using N2
 using N1
+using N2
 variables a b : num
 variable f : num → val
 coercion f

tests/lean/run/nat_coe.lean

@@ -0,0 +1,26 @@
+import logic
+
+variable nat : Type.{1}
+variable int : Type.{1}
+
+variable nat_add : nat → nat → nat
+infixl `+`:65 := nat_add
+
+variable int_add : int → int → int
+infixl `+`:65 := int_add
+
+variable of_nat : nat → int
+coercion of_nat
+
+variables a b : nat
+variables i j : int
+
+abbreviation c1 := a + b
+
+theorem T1 : c1 = nat_add a b :=
+refl _
+
+abbreviation c2 := i + j
+
+theorem T2 : c2 = int_add i j :=
+refl _