Library zoo_std.diverge

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base.
From zoo Require Import
  options.

Definition diverge : val :=
  rec: "diverge" ≠ ⇒
    "diverge" ().

Section zoo_G.
  Context `{zoo_G : !ZooG Σ}.

  Implicit Types Φ : val → iProp Σ.

  Lemma diverge𑁒spec E Φ :
    ⊢ WP diverge () @ E {{ Φ }}.

  #[global] Instance diverge𑁒diaspec E :
    DIASPEC
    {{
      True
    }}
      diverge ()%V @ E
    {{
      RET ();
      False
    }}.
End zoo_G.

#[global] Opaque diverge.