From 0ed3f08c1b446d45f87c4cb58b861144fd9981d0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 6 Mar 2021 14:36:22 -0800
Subject: [PATCH] feat: `open` in terms and tatics

See #330
---
 src/Lean/Elab/Tactic/Basic.lean    |  6 +++--
 src/Lean/Elab/Term.lean            |  2 --
 tests/lean/run/openTermTactic.lean | 37 ++++++++++++++++++++++++++++++
 3 files changed, 41 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/openTermTactic.lean

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 456f2e422c..4bdabfe0e7 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -305,8 +305,10 @@ def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVar
 @[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx =>
   focus $ evalTactic stx[1]
 
--- @[builtinTactic Lean.Parser.Tactic.«open»] def evalOpen : Tactic := fun stx =>
---   focus $ evalTactic stx[1]
+@[builtinTactic Parser.Tactic.open] def evalOpen : Tactic := fun stx => do
+  let openDecls ← elabOpenDecl stx[1]
+  withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
+    evalTactic stx[3]
 
 @[builtinTactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do
   let gs ← getUnsolvedGoals
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 890995fd5e..b0e3c24746 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1424,12 +1424,10 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
   | none     => throwIllFormedSyntax
   | some msg => elabTermEnsuringType stx[2] expectedType? true msg
 
-/- Uncomment after update stage0
 @[builtinTermElab «open»] def elabOpen : TermElab := fun stx expectedType? => do
   let openDecls ← elabOpenDecl stx[1]
   withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
     elabTerm stx[3] expectedType?
--/
 
 private def mkSomeContext : Context := {
   fileName      := "<TermElabM>"
diff --git a/tests/lean/run/openTermTactic.lean b/tests/lean/run/openTermTactic.lean
new file mode 100644
index 0000000000..101dde0ce0
--- /dev/null
+++ b/tests/lean/run/openTermTactic.lean
@@ -0,0 +1,37 @@
+def f (x : Nat) :=
+  open Nat in
+  succ (succ x)
+
+theorem f_eq : f x = Nat.succ (Nat.succ x) :=
+  rfl
+
+def g (x : Nat) := open Nat in succ (succ x)
+
+theorem f_eq_g : f x = g x := rfl
+
+def h (x : Nat) := Nat.succ (open Nat in succ x)
+
+theorem f_eq_h : f x = h x := rfl
+
+open Nat in
+def h' (x : Nat) := succ x
+
+theorem ex (x y : Nat) (h : x = y) : x + 1 = y + 1 := by
+  open Nat in show succ x = succ y
+  apply congrArg
+  assumption
+
+
+inductive InductiveWithAVeryLongName where
+  | c1 | c2 | c3 | c4 | c5 | c6 | c7
+
+def foo (e : InductiveWithAVeryLongName) : Type :=
+  open InductiveWithAVeryLongName in
+  match e with
+    | c1 => Nat
+    | c2 => Nat → Nat
+    | c3 => Nat → Nat → Nat
+    | c4 => Nat → Nat → Nat → Nat
+    | c5 => Nat → Nat → Nat → Nat → Nat
+    | c6 => Nat → Nat → Nat → Nat → Nat → Nat
+    | c7 => Nat → Nat → Nat → Nat → Nat → Nat → Nat