@@ -233,6 +233,12 @@ div left (S right) = div' left left right
233233 else
234234 S (div' left (centre - (S right)) right)
235235
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+
236242--------------------------------------------------------------------------------
237243-- Properties
238244--------------------------------------------------------------------------------