From iris.heap_lang Require Export notation.

Definition newbarrier : val := λ: <>, ref §0.
Definition signal : val := λ: "x", '"x" <- §1.
Definition wait : val :=
  rec: "wait" "x" := if: !'"x" = §1 then §() else '"wait" '"x".