Skip to content

Instantly share code, notes, and snippets.

@anton-trunov
Created Nov 22, 2016
Embed
What would you like to do?
Definition log2 n :=
let helper :=
(fix log2_helper n dummy :=
match dummy with
| 0 => 0
| S d' => match n with
| 0 | 1 => 0
| n => S (log2_helper (Nat.div2 n) d')
end
end) in
helper n n.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment