From 81dc201bab55bf49297e4eed2fcfd6f4232f8c33 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 26 Oct 2014 18:23:30 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): nested begin-end bug

---
 src/frontends/lean/elaborator.cpp |  2 +-
 tests/lean/run/nested_begin.lean  | 45 +++++++++++++++++++++++++++++++
 2 files changed, 46 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/nested_begin.lean

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index eab2e50cb6..e6921ac9fe 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1157,7 +1157,7 @@ static expr translate_local_name(environment const & env, list<expr> const & ctx
 */
 static expr translate(environment const & env, list<expr> const & ctx, expr const & e) {
     auto fn = [&](expr const & e) {
-        if (is_placeholder(e)) {
+        if (is_placeholder(e) || is_by(e)) {
             return some_expr(e); // ignore placeholders
         } else if (is_constant(e)) {
             if (!env.find(const_name(e))) {
diff --git a/tests/lean/run/nested_begin.lean b/tests/lean/run/nested_begin.lean
new file mode 100644
index 0000000000..60ab2c3dbc
--- /dev/null
+++ b/tests/lean/run/nested_begin.lean
@@ -0,0 +1,45 @@
+import logic data.nat.basic
+open nat
+
+inductive vector (A : Type) : nat → Type :=
+vnil  : vector A zero,
+vcons : Π {n : nat}, A → vector A n → vector A (succ n)
+
+namespace vector
+  definition no_confusion_type {A : Type} {n : nat} (P : Type) (v₁ v₂ : vector A n) : Type :=
+  cases_on v₁
+    (cases_on v₂
+      (P → P)
+      (λ n₂ h₂ t₂, P))
+    (λ n₁ h₁ t₁, cases_on v₂
+      P
+      (λ n₂ h₂ t₂, (Π (H : n₁ = n₂), h₁ = h₂ → eq.rec_on H t₁ = t₂ → P) → P))
+
+
+  definition no_confusion {A : Type} {n : nat} {P : Type} {v₁ v₂ : vector A n} : v₁ = v₂ → no_confusion_type P v₁ v₂ :=
+  assume H₁₂ : v₁ = v₂,
+    begin
+       show no_confusion_type P v₁ v₂, from
+       have aux : v₁ = v₁ → no_confusion_type P v₁ v₁, from
+        take H₁₁,
+          begin
+            apply (cases_on v₁),
+              exact (assume h : P, h),
+
+              intros (n, a, v, h),
+              apply (h rfl),
+              repeat (apply rfl)
+          end,
+        eq.rec_on H₁₂ aux H₁₂
+    end
+
+  theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ :=
+  begin
+     intro h, apply (no_confusion h), intros, assumption
+  end
+
+  theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ = v₂ :=
+  begin
+    intro h, apply (no_confusion h), intros, eassumption
+  end
+end vector