diff --git a/library/Init/Lean/Level.lean b/library/Init/Lean/Level.lean
index 5190f2cdb8..6c3da4e1f0 100644
--- a/library/Init/Lean/Level.lean
+++ b/library/Init/Lean/Level.lean
@@ -84,7 +84,7 @@ u.data.hasParam
 @[export lean_level_hash] def hashEx : Level → USize := hash
 @[export lean_level_has_mvar] def hasMVarEx : Level → Bool := hasMVar
 @[export lean_level_has_param] def hasParamEx : Level → Bool := hasParam
-@[export lean_level_depth] def depthEx : Level → Nat := depth
+@[export lean_level_depth] def depthEx (u : Level) : UInt32 := u.data.depth
 
 end Level