From cca7e4f97c5d136b1a3f34bfd3877599154afe69 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Mon, 13 Apr 2026 19:32:44 +0200
Subject: [PATCH] scoped delab

---
 KernelHom/Tactic/Delaborators.lean | 12 +++++++-----
 KernelHom/Tests/Examples.lean      |  2 +-
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/KernelHom/Tactic/Delaborators.lean b/KernelHom/Tactic/Delaborators.lean
index a6b08d54d..b56641a42 100644
--- a/KernelHom/Tactic/Delaborators.lean
+++ b/KernelHom/Tactic/Delaborators.lean
@@ -12,29 +12,31 @@ import Lean
 
 This file implements delaborators that provide simplified pretty-printing kernel-related
 categorical operations that are generated using the `kernel_hom` tactic.
+
+To use these delaborators, simply open the `KernelHom` namespace.
 -/
 
 open Lean Meta Elab Command PrettyPrinter Delaborator
 open Lean.PrettyPrinter.Delaborator.SubExpr
 
-namespace KernelHom.Delaborators
+namespace KernelHom
 
 /-- Removes the `ULift` wrapper for readability. -/
-@[app_delab ULift]
+@[scoped app_delab ULift]
 meta def delabULift : Delab := do
   let x ← withNaryArg 0 delab
   `($x)
 
 /-- Only display the carrier space of `SFinKer.of` for readability. -/
-@[app_delab SFinKer.of]
+@[scoped app_delab SFinKer.of]
 meta def delabSFinKerOf : Delab := do
   let x ← withNaryArg 0 delab
   `($x)
 
 /-- Only display the underlying kernel of `Kernel.hom` for readability. -/
-@[app_delab ProbabilityTheory.Kernel.hom]
+@[scoped app_delab ProbabilityTheory.Kernel.hom]
 meta def delabKernelHom : Delab := do
   let x ← withNaryArg 10 delab
   `($x)
 
-end KernelHom.Delaborators
+end KernelHom
diff --git a/KernelHom/Tests/Examples.lean b/KernelHom/Tests/Examples.lean
index 74e3ecd3b..0215e01f1 100644
--- a/KernelHom/Tests/Examples.lean
+++ b/KernelHom/Tests/Examples.lean
@@ -8,7 +8,7 @@ import KernelHom.Tactic.Tactics
 
 open MeasureTheory ProbabilityTheory CategoryTheory BraidedCategory
 
-open scoped MonoidalCategory ComonObj
+open scoped MonoidalCategory ComonObj KernelHom
 
 variable {X Y Z T X' Y' Z' : Type*} [MeasurableSpace X] [MeasurableSpace Y]
   [MeasurableSpace Z] [MeasurableSpace T] [MeasurableSpace X'] [MeasurableSpace Y']