From d88813feffb7f49db03fd8fabe857838614710eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 17 Nov 2019 08:51:42 -0800 Subject: [PATCH] fix: `lean_level_depth` export --- library/Init/Lean/Level.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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