Library zoo_std.assert

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 assert : val :=
  fun: "b" ⇒
    if: ¬ "b" then
      Fail.

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

  Lemma assert𑁒spec (b : bool) Φ :
    b = true →
    ▷ Φ ()%V -∗
    WP assert #b {{ Φ }}.
End zoo_G.

#[global] Opaque assert.