Skip to content

Instantly share code, notes, and snippets.

@anton-trunov

anton-trunov/log2n.v

Created November 22, 2016 18:29
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • 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.
Download ZIP
Raw
log2n.v
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