Library hydras.Prelude.Fuel

From Coq Require Import FunInd Recdef Wf_nat Lia.

Function zero (n:nat) {wf lt n} : nat :=
  match n with
    0 ⇒ 0
  | S n' as p ⇒ zero (Nat.div2 p)
  end.


About lt_wf.

Module OpaqueWf.

 Lemma lt_wf : well_founded lt.

  Function zero (n:nat) {wf lt n} : nat :=
    match n with
      0 ⇒ 0
    | _ ⇒ zero (Nat.div2 n)
    end.

About Acc_intro_generator.


Function zero' (n:nat) {wf lt n} : nat :=
  match n with
    0 ⇒ 0
  | _ ⇒ zero' (Nat.div2 n)
  end.


End OpaqueWf.


Inductive fuel :=
 | FO : fuel
 | FS : (unit → fuel) → fuel.


Fixpoint foo (n:nat) x :=
 match n with
 | S n ⇒ FS (fun _ ⇒ foo n (foo n x))
 | O ⇒ x
 end.