From 049b7790c9aa19cc8d93a0c90dee37742d25350e Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 21 Oct 2024 10:39:46 +1100
Subject: [PATCH] fix tests

---
 test/Lint.lean | 19 ++++---------------
 1 file changed, 4 insertions(+), 15 deletions(-)

diff --git a/test/Lint.lean b/test/Lint.lean
index 6ae7301e48199..391ff9dc09d60 100644
--- a/test/Lint.lean
+++ b/test/Lint.lean
@@ -2,26 +2,13 @@ import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.ToAdditive
 import Mathlib.Order.SetNotation
 
--- TODO: the linter also runs on the #guard_msg, so disable it once
--- See https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/.23guard_msgs.20doesn't.20silence.20warnings/near/423534679
-
-set_option linter.dupNamespace false
-
 namespace termG
+
 -- this creates a hygienic declaration starting with `termG.termG.«_@».test.Lint...`
 -- and the linter ignores it
 set_option linter.dupNamespace true in
 local notation "G" => Unit
 
-/-- info: [termG, termG] -/
-#guard_msgs in
-open Lean in
-run_meta
-  let env ← getEnv
-  let consts := env.constants.toList.find? (·.1.getRoot == `termG)
-  let reps := (consts.map (·.1.components.take 2)).getD default
-  logInfo m!"{reps}"
-  guard (reps[0]! == reps[1]!)
 end termG
 
 /--
@@ -70,9 +57,11 @@ namespace add
 /--
 warning: The namespace 'add' is duplicated in the declaration 'add.add'
 note: this linter can be disabled with `set_option linter.dupNamespace false`
+---
+warning: The namespace 'add' is duplicated in the declaration 'add.add'
+note: this linter can be disabled with `set_option linter.dupNamespace false`
 -/
 #guard_msgs in
-set_option linter.dupNamespace true in
 export Nat (add add_comm add)
 
 end add