Commit 2025-01-22 23:41 3dc2beff
View on Github →feat(Data/Nat): faster computation of Nat.log (#17325)
Give an alternate definition Nat.logC for Nat.log which computes more efficiently (roughly speaking, this should have logarithmic time in the output, while Nat.log has linear time in its output).
Prove that these two give the same output, and use csimp to ensure evaluation of Nat.log uses Nat.logC instead.