(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module native_mint.
  Definition value_DECIMALS : Value.t := M.run ltac:(M.monadic (M.alloc (| Value.Integer 9 |))).
  
  Definition value_ID : Value.t :=
    M.run
      ltac:(M.monadic
        (M.alloc (|
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "solana_program::pubkey::Pubkey",
              "new_from_array",
              []
            |),
            [
              Value.Array
                [
                  Value.Integer 131;
                  Value.Integer 13;
                  Value.Integer 252;
                  Value.Integer 159;
                  Value.Integer 222;
                  Value.Integer 95;
                  Value.Integer 230;
                  Value.Integer 184;
                  Value.Integer 170;
                  Value.Integer 124;
                  Value.Integer 4;
                  Value.Integer 164;
                  Value.Integer 118;
                  Value.Integer 233;
                  Value.Integer 30;
                  Value.Integer 138;
                  Value.Integer 198;
                  Value.Integer 187;
                  Value.Integer 38;
                  Value.Integer 74;
                  Value.Integer 173;
                  Value.Integer 144;
                  Value.Integer 250;
                  Value.Integer 25;
                  Value.Integer 201;
                  Value.Integer 223;
                  Value.Integer 73;
                  Value.Integer 216;
                  Value.Integer 92;
                  Value.Integer 62;
                  Value.Integer 91;
                  Value.Integer 94
                ]
            ]
          |)
        |))).
  
  (* solana_program::declare_id!("9pan9bMn5HatX4EJdBwg9VgCa7Uz5HL8N1m5D3NdXejP") *)
  Definition check_id (τ : list Ty.t) (α : list Value.t) : M :=
    match τ, α with
    | [], [ id ] =>
      ltac:(M.monadic
        (let id := M.alloc (| id |) in
        M.call_closure (|
          M.get_trait_method (|
            "core::cmp::PartialEq",
            Ty.apply (Ty.path "&") [ Ty.path "solana_program::pubkey::Pubkey" ],
            [ Ty.apply (Ty.path "&") [ Ty.path "solana_program::pubkey::Pubkey" ] ],
            "eq",
            []
          |),
          [ id; M.alloc (| M.get_constant (| "spl_token_2022::native_mint::ID" |) |) ]
        |)))
    | _, _ => M.impossible
    end.
  
  (* solana_program::declare_id!("9pan9bMn5HatX4EJdBwg9VgCa7Uz5HL8N1m5D3NdXejP") *)
  Definition id (τ : list Ty.t) (α : list Value.t) : M :=
    match τ, α with
    | [], [] =>
      ltac:(M.monadic (M.read (| M.get_constant (| "spl_token_2022::native_mint::ID" |) |)))
    | _, _ => M.impossible
    end.
  
  Definition value_PROGRAM_ADDRESS_SEEDS : Value.t :=
    M.run
      ltac:(M.monadic
        (M.alloc (|
          (* Unsize *)
          M.pointer_coercion
            (M.alloc (|
              Value.Array
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                    [ M.read (| Value.String "native-mint" |) ]
                  |);
                  (* Unsize *) M.pointer_coercion (M.alloc (| Value.Array [ Value.Integer 255 ] |))
                ]
            |))
        |))).
End native_mint.
