max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: lean_level_depth export

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-17 08:51:42 -08:00
parent 66895b2c94
commit d88813feff
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/Init/Lean/Level.lean
View file

@ -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