Fix bug in the elaborator. Move character ' to class A

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

src/frontends/lean/lean_elaborator.cpp

@@ -470,7 +470,9 @@ class elaborator::imp {
 
     void unify_simple_ho_match(expr const & e1, expr const & e2, constraint const & c) {
         context const & ctx = c.m_ctx;
-        m_constraints.push_back(constraint(arg(e1,0), mk_lambda(car(ctx).get_name(), car(ctx).get_domain(), e2), c));
+        m_constraints.push_back(constraint(arg(e1,0), mk_lambda(car(ctx).get_name(),
+                                                           lift_free_vars_mmv(car(ctx).get_domain(), 1, 1),
+                                                           lift_free_vars_mmv(e2, 1, 1)), c));
     }
 
     struct cycle_detected {};

src/frontends/lean/lean_scanner.cpp

@@ -51,6 +51,7 @@ public:
             set(i, 'a');
 
         set('_',  'a');
+        set('\'', 'a');
 
         // characters that can be used to create ids of group b
         for (unsigned char b : {'=', '<', '>', '@', '^', '|', '&', '~', '+', '-', '*', '/', '\\', '$', '%', '?', ';', '[', ']'})

tests/lean/elab2.lean

@@ -0,0 +1,25 @@
+
+Variable C : Pi (A B : Type) (H : A = B) (a : A), B
+
+Variable D : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
+
+Variable R : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
+             (B a) = (B' (C A A' (D A A' B B' H) a))
+
+Theorem R2 (A A' B B' : Type) (H : A -> B = A' -> B') (a : A) : B = B' := R _ _ _ _ H a
+
+Show Environment 1
+
+Theorem R3 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
+    fun (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1),
+        R _ _ _ _ H a
+
+Theorem R4 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
+    fun (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : _),
+        R _ _ _ _ H a
+
+Theorem R5 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
+    fun (A1 A2 B1 B2 : Type) (H : _) (a : _),
+        R _ _ _ _ H a
+
+Show Environment 1

tests/lean/elab2.lean.expected.out

@@ -0,0 +1,12 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: C
+  Assumed: D
+  Assumed: R
+  Proved: R2
+Theorem R2 (A A' B B' : Type) (H : A → B = A' → B') (a : A) : B = B' := R A A' (λ x : A, B) (λ x : A', B') H a
+  Proved: R3
+  Proved: R4
+  Proved: R5
+Theorem R5 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
+    R A1 A2 (λ a : A1, B1) (λ _ : A2, B2) H a