clean up uses of open

Author: awalterschulze

Validator/Env/TestEnvTreeParserStateWithMem.lean

@@ -13,8 +13,6 @@ structure TreeParserAndMemTest where
   enter: MemEnter.EnterMap
   leave: MemLeave.LeaveMap
 
-open EnvTreeParserStateWithMem
-
 abbrev TreeParserStateWithMemTest α := EStateM String TreeParserAndMemTest α
 
 def TreeParserStateWithMemTest.mk (p: TreeParser.TreeParser): TreeParserAndMemTest :=

Validator/Expr/Language.lean

@@ -4,7 +4,19 @@ import Validator.Std.Linter.DetectClassical
 
 namespace Language
 
-open List
+open List (
+  append_assoc
+  append_eq_nil_iff
+  append_nil
+  cons
+  cons_append
+  cons.injEq
+  foldl_nil
+  nil
+  nil_append
+  nil_eq
+  singleton_append
+)
 
 -- Definitions
 

Validator/Parser/TreeParser.lean

@@ -126,8 +126,7 @@ def TreeParser.run (x: StateT TreeParser (Except String) α) (t: ParseTree): Exc
 instance : Debug (StateT TreeParser (Except String)) where
   debug (_: String) := return ()
 
-open Parser (walk)
-open Parser (Action)
+open Parser (walk Action)
 open ParseTree (node)
 
 #guard TreeParser.run

Validator/Std/Linter/DetectClassical.lean

@@ -12,7 +12,9 @@ The "detectClassical" linter emits a warning on declarations that depend on the
 axiom.
 -/
 
-open Lean Elab Command
+open Lean (Linter collectAxioms logInfoAt addLinter withSetOptionIn)
+open Lean.Linter (getLinterOptions getLinterValue logLint)
+open Mathlib.Linter (getNamesFrom)
 
 namespace RegexDeriv.Std.Linter
 
@@ -38,14 +40,14 @@ namespace DetectClassical
 
 @[inherit_doc RegexDeriv.Std.Linter.linter.detectClassical]
 def detectClassicalLinter : Linter where run := withSetOptionIn fun stx ↦ do
-  unless Linter.getLinterValue linter.detectClassical (← Linter.getLinterOptions) do
+  unless getLinterValue linter.detectClassical (← getLinterOptions) do
     return
   if (← get).messages.hasErrors then
     return
   let d := (stx.getPos?.getD default)
-  let nmsd := (← Mathlib.Linter.getNamesFrom d)
+  let nmsd := (← getNamesFrom d)
   let nms := nmsd.filter (! ·.getId.isInternal)
-  let verbose? := Linter.getLinterValue linter.verbose.detectClassical (← Linter.getLinterOptions)
+  let verbose? := getLinterValue linter.verbose.detectClassical (← getLinterOptions)
   for constStx in nms do
     let constName := constStx.getId
     let axioms ← collectAxioms constName
@@ -58,7 +60,7 @@ def detectClassicalLinter : Linter where run := withSetOptionIn fun stx ↦ do
         logInfoAt constStx
           m!"'{constName}' is non-classical and depends on axioms: {axioms.toList}"
     else
-      Linter.logLint linter.detectClassical constStx
+      logLint linter.detectClassical constStx
         m!"'{constName}' depends on 'Classical.choice' on axioms: {axioms.toList}"
 
 initialize addLinter detectClassicalLinter