Library examples.future_fibonacci

Require Import zoo.prelude.
Require Import zoo.base.
Require Export examples.fibonacci.
Require Export examples.future_fibonacci__code.
Require Import examples.future_fibonacci__types.
Require Import zoo.options.

Section future۰G.
  Context `{future۰G : FutureG Σ}.

  #[local] Lemma future_fibonacci٠main₁ｰspec n pool ctx scope :
    (0 ≤ n)%Z →
    {{{
      pool۰context pool ctx scope
    }}}
      future_fibonacci٠main₁ ctx #n
    {{{
      RET #(fibonacci ₊n);
      pool۰context pool ctx scope
    }}}.
  Lemma future_fibonacci٠mainｰspec (num_dom n : nat) :
    {{{
      True
    }}}
      future_fibonacci٠main #num_dom #n
    {{{
      RET #(fibonacci n);
      True
    }}}.
End future۰G.

Require examples.future_fibonacci__opaque.