Library examples.future_fibonacci

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_parabs Require Import
  future
  pool.
From examples Require Export
  fibonacci
  future_fibonacci__code.
From zoo Require Import
  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.

From examples Require
  future_fibonacci__opaque.