diff --git a/src/Init/Data/Nat/Log2.lean b/src/Init/Data/Nat/Log2.lean index cadf4db9d3..59162e7775 100644 --- a/src/Init/Data/Nat/Log2.lean +++ b/src/Init/Data/Nat/Log2.lean @@ -35,7 +35,7 @@ Examples: * `Nat.log2 7 = 2` * `Nat.log2 8 = 3` -/ -@[extern "lean_nat_log2"] +@[expose, extern "lean_nat_log2"] def log2 (n : @& Nat) : Nat := -- Lean "assembly" n.rec (fun _ => nat_lit 0) (fun _ ih n =>