From 2cd21e08ba2cc07b48cf2f9c07c9647704cd56f4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 24 Oct 2022 08:19:30 -0700
Subject: [PATCH] chore: add `CollectLevelParams.visitLevels`

---
 src/Lean/Util/CollectLevelParams.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Util/CollectLevelParams.lean b/src/Lean/Util/CollectLevelParams.lean
index 82ae8170fb..54db73fb4c 100644
--- a/src/Lean/Util/CollectLevelParams.lean
+++ b/src/Lean/Util/CollectLevelParams.lean
@@ -31,6 +31,9 @@ mutual
     | _          => id
 end
 
+def visitLevels (us : List Level) : Visitor :=
+  fun s => us.foldl (fun s u => visitLevel u s) s
+
 mutual
   partial def visitExpr (e : Expr) : Visitor := fun s =>
     if !e.hasLevelParam then s
@@ -44,7 +47,7 @@ mutual
     | .letE _ t v b _  => visitExpr b ∘ visitExpr v ∘ visitExpr t
     | .app f a         => visitExpr a ∘ visitExpr f
     | .mdata _ b       => visitExpr b
-    | .const _ us      => fun s => us.foldl (fun s u => visitLevel u s) s
+    | .const _ us      => visitLevels us
     | .sort u          => visitLevel u
     | _                => id
 end