From 0a54391ebaa22bc38d534d8fe29e595c8af5b7f3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 13 Aug 2020 16:20:25 -0700
Subject: [PATCH] chore: add helper

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

diff --git a/src/Lean/Util/CollectLevelParams.lean b/src/Lean/Util/CollectLevelParams.lean
index 2b417436fc..e4882371b9 100644
--- a/src/Lean/Util/CollectLevelParams.lean
+++ b/src/Lean/Util/CollectLevelParams.lean
@@ -61,4 +61,7 @@ end CollectLevelParams
 def collectLevelParams (s : CollectLevelParams.State) (e : Expr) : CollectLevelParams.State :=
 CollectLevelParams.main e s
 
+def CollectLevelParams.State.collect (s : CollectLevelParams.State) (e : Expr) : CollectLevelParams.State :=
+collectLevelParams s e
+
 end Lean