git.iko.soy/Idris-dev
on master help sign in
flooring log2 for Nats
103d65eBenjamin Saunders
lib/Prelude/Nat.idr+6
compare with master
unifiedsplit
@@ -233,6 +233,12 @@ div left (S right) = div' left left right
233 else
233 else
234 S (div' left (centre - (S right)) right)
234 S (div' left (centre - (S right)) right)
235
235
236+%assert_total
237+log2 : Nat -> Nat
238+log2 O = O
239+log2 (S O) = O
240+log2 n = S (log2 (n `div` 2))
241+
236--------------------------------------------------------------------------------
242--------------------------------------------------------------------------------
237-- Properties
243-- Properties
238--------------------------------------------------------------------------------
244--------------------------------------------------------------------------------