fix(frontends/lean/parser): fixes #770

src/frontends/lean/parser.cpp

@@ -1418,7 +1418,7 @@ expr parser::parse_numeral_expr(bool user_notation) {
     }
     buffer<expr> cs;
     if (*m_has_num)
-        cs.push_back(save_pos(from_num(n), p));
+        cs.push_back(save_pos(copy(from_num(n)), p));
     for (expr const & c : vals)
         cs.push_back(copy_with_new_pos(c, p));
     // Remark: choices are processed from right to left.

tests/lean/770.hlean

@@ -0,0 +1,20 @@
+open nat unit equiv eq
+
+  definition code : ℕ → ℕ → Type₀
+  | code 0 0 := unit
+  | code (succ n) 0 := empty
+  | code 0 (succ m) := empty
+  | code (succ n) (succ m) := code n m
+
+  definition refl : Πn, code n n
+  | refl 0 := star
+  | refl (succ n) := refl n
+
+
+  definition encode (n m : ℕ) : (n = m) ≃ code n m :=
+  equiv.MK (λp, sorry) -- p ▸ refl n)
+           (match n m with
+            | 0 0 := sorry
+            end)
+           sorry
+           sorry

tests/lean/770.hlean.expected.out

@@ -0,0 +1,2 @@
+770.hlean:17:14: error: function expected at
+  0