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

chore: expose Nat.log2 (#11401)

Browse source 
Necessary for kernel reduction of `binaryRec`, see
leanprover-community/mathlib4#30144
This commit is contained in:
Junyan Xu 2025-12-14 06:19:29 +01:00 • committed by GitHub
parent c20378682e
commit fb6c96e54b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/Nat/Log2.lean
View file

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