diff --git a/src/Lean/Elab/Open.lean b/src/Lean/Elab/Open.lean index a00bec0cbe..b473180cfc 100644 --- a/src/Lean/Elab/Open.lean +++ b/src/Lean/Elab/Open.lean @@ -39,6 +39,11 @@ private def elabOpenSimple (n : Syntax) : M (m:=m) Unit := addOpenDecl (OpenDecl.simple ns []) activateScoped ns +private def elabOpenScoped (n : Syntax) : M (m:=m) Unit := + -- `open` `scoped` id+ + for ns in n[1].getArgs do + activateScoped (← resolveNamespace ns.getId) + -- `open` id `(` id+ `)` private def elabOpenOnly (n : Syntax) : M (m:=m) Unit := do let ns ← resolveNamespace n[0].getId @@ -69,6 +74,8 @@ def elabOpenDecl [MonadResolveName m] (openDeclStx : Syntax) : m (List OpenDecl) StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do if openDeclStx.getKind == ``Parser.Command.openSimple then elabOpenSimple openDeclStx + else if openDeclStx.getKind == ``Parser.Command.openScoped then + elabOpenScoped openDeclStx else if openDeclStx.getKind == ``Parser.Command.openOnly then elabOpenOnly openDeclStx else if openDeclStx.getKind == ``Parser.Command.openHiding then diff --git a/tests/lean/openScoped.lean b/tests/lean/openScoped.lean new file mode 100644 index 0000000000..c030cde018 --- /dev/null +++ b/tests/lean/openScoped.lean @@ -0,0 +1,25 @@ +#check @epsilon -- Error + +noncomputable def foo1 (f g : Nat → Nat) : Nat := + if f = g then 1 else 2 -- Error + +section +open Classical + +#check @epsilon + +noncomputable def foo2 (f g : Nat → Nat) : Nat := + if f = g then 1 else 2 -- Ok +end + +#check @epsilon -- Error + +section + +open scoped Classical +#check @epsilon -- Error + +noncomputable def foo3 (f g : Nat → Nat) : Nat := + if f = g then 1 else 2 -- Ok + +end diff --git a/tests/lean/openScoped.lean.expected.out b/tests/lean/openScoped.lean.expected.out new file mode 100644 index 0000000000..98d19f3dc5 --- /dev/null +++ b/tests/lean/openScoped.lean.expected.out @@ -0,0 +1,6 @@ +openScoped.lean:1:8-1:15: error: unknown identifier 'epsilon' +openScoped.lean:4:2-4:24: error: failed to synthesize instance + Decidable (f = g) +epsilon : {α : Sort u_1} → [h : Nonempty α] → (α → Prop) → α +openScoped.lean:15:8-15:15: error: unknown identifier 'epsilon' +openScoped.lean:20:8-20:15: error: unknown identifier 'epsilon'