Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Definition log2 :=
well_founded_induction Wf_nat.lt_wf (fun _ => nat)
(fun n => match n return ((forall y : nat, (y < n) -> nat) -> nat) with
| 0 => fun _ => 0
| 1 => fun _ => 0
| n => fun self => S (self (Nat.div2 n)
(Nat.lt_div2 _ (lt_0_Sn _)))
end).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment