Library zoo_std.ivar_1__code

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

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

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

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

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

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

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

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