Skip to content

Instantly share code, notes, and snippets.

@anton-trunov
Created November 22, 2016 18:29
Show Gist options
  • Save anton-trunov/c3144d1a6e11ac023b65be6d36bf3253 to your computer and use it in GitHub Desktop.
Save anton-trunov/c3144d1a6e11ac023b65be6d36bf3253 to your computer and use it in GitHub Desktop.
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