chore: close namespace

opencompl · Feb 14, 2025 · 2ad8b1c · 2ad8b1c
1 parent 20988c9
commit 2ad8b1c
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean
@@ -389,3 +389,5 @@ def bvAcNormalizePass : Pass where
       if let .some nextGoal ← bvAcNfHypMeta newGoal hyp then
         newGoal := nextGoal
     return newGoal
+
+end Frontend.Normalize