Library zoo_std.mvar__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo.options.

Definition mvarู create : val :=
  ๐—ณ๐˜‚๐—ป โŽฝ โ†’
    ๐—ฟ๐—ฒ๐—ณ ยงNone.

Definition mvarู make : val :=
  ๐—ณ๐˜‚๐—ป "v" โ†’
    ๐—ฟ๐—ฒ๐—ณ โ€˜Some( "v" ).

Definition mvarู try_get : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    !"t".

Definition mvarู is_unset : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    mvarู try_get "t" == ยงNone.

Definition mvarู is_set : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    ยฌ mvarู is_unset "t".

Definition mvarู get : val :=
  ๐—ณ๐˜‚๐—ป "t" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต mvarู try_get "t" ๐˜„๐—ถ๐˜๐—ต
    | None โ†’
        ๐—ณ๐—ฎ๐—ถ๐—น
    | Some "v" โ†’
        "v"
    ๐—ฒ๐—ป๐—ฑ.

Definition mvarู set : val :=
  ๐—ณ๐˜‚๐—ป "t" "v" โ†’
    "t" <- โ€˜Some( "v" ).