From fb6c96e54bc3b27fb7d7fbd1c7c2bfa950af2837 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Sun, 14 Dec 2025 06:19:29 +0100
Subject: [PATCH] chore: expose `Nat.log2` (#11401)

Necessary for kernel reduction of `binaryRec`, see
leanprover-community/mathlib4#30144
---
 src/Init/Data/Nat/Log2.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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