Library zoo.program_logic.diverge

Require Import zoo.prelude.
Require Import zoo.base.
Require Import zoo.options.

Definition diverge : val :=
  π—Ώπ—²π—° "diverge" ⎽ β†’
    "diverge" ().

Notation "'π—±π—Άπ˜ƒπ—²π—Ώπ—΄π—²'" :=
  diverge
: expr_scope.

Section zooΫ°G.
  Context `{zooΫ°G : !ZooG Ξ£}.

  Implicit Type Ξ¦ : val β†’ iProp Ξ£.

  Lemma divergeο½°spec E Ξ¦ :
    βŠ’ WP π—±π—Άπ˜ƒπ—²π—Ώπ—΄π—² () @ E {{ Ξ¦ }}.

  #[global] Instance divergeο½°diaspec E :
    DIASPEC
    {{
      True
    }}
      π—±π—Άπ˜ƒπ—²π—Ώπ—΄π—² ()%V @ E
    {{
      RET ();
      False
    }}.
End zooΫ°G.

#[global] Opaque diverge.