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

(* StructRecord
  {
    name := "Mapping";
    const_params := [];
    ty_params := [ "K"; "V" ];
    fields :=
      [
        ("_key", Ty.apply (Ty.path "core::marker::PhantomData") [] [ K ]);
        ("_value", Ty.apply (Ty.path "core::marker::PhantomData") [] [ V ])
      ];
  } *)

Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_erc721_Mapping_K_V.
  Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc721::Mapping") [] [ K; V ].
  
  (* Default *)
  Definition default (K V : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self K V in
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "erc721::Mapping"
          [
            ("_key",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply (Ty.path "core::marker::PhantomData") [] [ K ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("_value",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply (Ty.path "core::marker::PhantomData") [] [ V ],
                  [],
                  "default",
                  []
                |),
                []
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    forall (K V : Ty.t),
    M.IsTraitInstance
      "core::default::Default"
      (Self K V)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method (default K V)) ].
End Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_erc721_Mapping_K_V.

Module Impl_erc721_Mapping_K_V.
  Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "erc721::Mapping") [] [ K; V ].
  
  (*
      fn contains(&self, _key: &K) -> bool {
          unimplemented!()
      }
  *)
  Parameter contains : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_contains :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "contains" (contains K V).
  
  (*
      fn get(&self, _key: &K) -> Option<V> {
          unimplemented!()
      }
  *)
  Parameter get : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_get :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "get" (get K V).
  
  (*
      fn insert(&mut self, _key: K, _value: V) -> Option<u32> {
          unimplemented!()
      }
  *)
  Parameter insert : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_insert :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "insert" (insert K V).
  
  (*
      fn remove(&self, _key: K) {
          unimplemented!()
      }
  *)
  Parameter remove : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_remove :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "remove" (remove K V).
  
  (*
      fn size(&self, _key: K) -> Option<u32> {
          unimplemented!()
      }
  *)
  Parameter size : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_size :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "size" (size K V).
  
  (*
      fn take(&self, _key: K) -> Option<V> {
          unimplemented!()
      }
  *)
  Parameter take : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_take :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "take" (take K V).
End Impl_erc721_Mapping_K_V.

(* StructTuple
  {
    name := "AccountId";
    const_params := [];
    ty_params := [];
    fields := [ Ty.path "u128" ];
  } *)

Module Impl_core_default_Default_for_erc721_AccountId.
  Definition Self : Ty.t := Ty.path "erc721::AccountId".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructTuple
          "erc721::AccountId"
          [
            M.call_closure (|
              M.get_trait_method (| "core::default::Default", Ty.path "u128", [], "default", [] |),
              []
            |)
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::default::Default"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method default) ].
End Impl_core_default_Default_for_erc721_AccountId.

Module Impl_core_clone_Clone_for_erc721_AccountId.
  Definition Self : Ty.t := Ty.path "erc721::AccountId".
  
  (* Clone *)
  Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          M.match_operator (|
            Value.DeclaredButUndefined,
            [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::clone::Clone"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("clone", InstanceField.Method clone) ].
End Impl_core_clone_Clone_for_erc721_AccountId.

Module Impl_core_marker_Copy_for_erc721_AccountId.
  Definition Self : Ty.t := Ty.path "erc721::AccountId".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_erc721_AccountId.

Module Impl_core_marker_StructuralPartialEq_for_erc721_AccountId.
  Definition Self : Ty.t := Ty.path "erc721::AccountId".
  
  Axiom Implements :
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_erc721_AccountId.

Module Impl_core_cmp_PartialEq_for_erc721_AccountId.
  Definition Self : Ty.t := Ty.path "erc721::AccountId".
  
  (* PartialEq *)
  Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        BinOp.eq (|
          M.read (|
            M.SubPointer.get_struct_tuple_field (| M.read (| self |), "erc721::AccountId", 0 |)
          |),
          M.read (|
            M.SubPointer.get_struct_tuple_field (| M.read (| other |), "erc721::AccountId", 0 |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("eq", InstanceField.Method eq) ].
End Impl_core_cmp_PartialEq_for_erc721_AccountId.

Module Impl_core_convert_From_array_Usize_32_u8_for_erc721_AccountId.
  Definition Self : Ty.t := Ty.path "erc721::AccountId".
  
  (*
      fn from(_value: [u8; 32]) -> Self {
          unimplemented!()
      }
  *)
  Parameter from : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::convert::From"
      Self
      (* Trait polymorphic types *)
      [ (* T *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ] ]
      (* Instance *) [ ("from", InstanceField.Method from) ].
End Impl_core_convert_From_array_Usize_32_u8_for_erc721_AccountId.

Axiom Balance : (Ty.path "erc721::Balance") = (Ty.path "u128").

(* StructRecord
  {
    name := "Env";
    const_params := [];
    ty_params := [];
    fields := [ ("caller", Ty.path "erc721::AccountId") ];
  } *)

Axiom TokenId : (Ty.path "erc721::TokenId") = (Ty.path "u32").

(* StructRecord
  {
    name := "Erc721";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("token_owner",
          Ty.apply (Ty.path "erc721::Mapping") [] [ Ty.path "u32"; Ty.path "erc721::AccountId" ]);
        ("token_approvals",
          Ty.apply (Ty.path "erc721::Mapping") [] [ Ty.path "u32"; Ty.path "erc721::AccountId" ]);
        ("owned_tokens_count",
          Ty.apply (Ty.path "erc721::Mapping") [] [ Ty.path "erc721::AccountId"; Ty.path "u32" ]);
        ("operator_approvals",
          Ty.apply
            (Ty.path "erc721::Mapping")
            []
            [ Ty.tuple [ Ty.path "erc721::AccountId"; Ty.path "erc721::AccountId" ]; Ty.tuple [] ])
      ];
  } *)

Module Impl_core_default_Default_for_erc721_Erc721.
  Definition Self : Ty.t := Ty.path "erc721::Erc721".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "erc721::Erc721"
          [
            ("token_owner",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "erc721::Mapping")
                    []
                    [ Ty.path "u32"; Ty.path "erc721::AccountId" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("token_approvals",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "erc721::Mapping")
                    []
                    [ Ty.path "u32"; Ty.path "erc721::AccountId" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("owned_tokens_count",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "erc721::Mapping")
                    []
                    [ Ty.path "erc721::AccountId"; Ty.path "u32" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("operator_approvals",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "erc721::Mapping")
                    []
                    [
                      Ty.tuple [ Ty.path "erc721::AccountId"; Ty.path "erc721::AccountId" ];
                      Ty.tuple []
                    ],
                  [],
                  "default",
                  []
                |),
                []
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::default::Default"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method default) ].
End Impl_core_default_Default_for_erc721_Erc721.

(*
Enum Error
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "NotOwner";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "NotApproved";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "TokenExists";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "TokenNotFound";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "CannotInsert";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "CannotFetchValue";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "NotAllowed";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

Module Impl_core_marker_StructuralPartialEq_for_erc721_Error.
  Definition Self : Ty.t := Ty.path "erc721::Error".
  
  Axiom Implements :
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_erc721_Error.

Module Impl_core_cmp_PartialEq_for_erc721_Error.
  Definition Self : Ty.t := Ty.path "erc721::Error".
  
  (* PartialEq *)
  Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        M.read (|
          let~ __self_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "erc721::Error" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "erc721::Error" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("eq", InstanceField.Method eq) ].
End Impl_core_cmp_PartialEq_for_erc721_Error.

Module Impl_core_cmp_Eq_for_erc721_Error.
  Definition Self : Ty.t := Ty.path "erc721::Error".
  
  (* Eq *)
  Definition assert_receiver_is_total_eq
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        Value.Tuple []))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Eq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
End Impl_core_cmp_Eq_for_erc721_Error.

Module Impl_core_clone_Clone_for_erc721_Error.
  Definition Self : Ty.t := Ty.path "erc721::Error".
  
  (* Clone *)
  Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (| M.read (| self |) |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::clone::Clone"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("clone", InstanceField.Method clone) ].
End Impl_core_clone_Clone_for_erc721_Error.

Module Impl_core_marker_Copy_for_erc721_Error.
  Definition Self : Ty.t := Ty.path "erc721::Error".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_erc721_Error.

(* StructRecord
  {
    name := "Transfer";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("from", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "erc721::AccountId" ]);
        ("to", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "erc721::AccountId" ]);
        ("id", Ty.path "u32")
      ];
  } *)

(* StructRecord
  {
    name := "Approval";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("from", Ty.path "erc721::AccountId");
        ("to", Ty.path "erc721::AccountId");
        ("id", Ty.path "u32")
      ];
  } *)

(* StructRecord
  {
    name := "ApprovalForAll";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("owner", Ty.path "erc721::AccountId");
        ("operator", Ty.path "erc721::AccountId");
        ("approved", Ty.path "bool")
      ];
  } *)

(*
Enum Event
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Transfer";
        item := StructTuple [ Ty.path "erc721::Transfer" ];
        discriminant := None;
      };
      {
        name := "Approval";
        item := StructTuple [ Ty.path "erc721::Approval" ];
        discriminant := None;
      };
      {
        name := "ApprovalForAll";
        item := StructTuple [ Ty.path "erc721::ApprovalForAll" ];
        discriminant := None;
      }
    ];
}
*)

Module Impl_erc721_Env.
  Definition Self : Ty.t := Ty.path "erc721::Env".
  
  (*
      fn caller(&self) -> AccountId {
          self.caller
      }
  *)
  Definition caller (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          M.SubPointer.get_struct_record_field (| M.read (| self |), "erc721::Env", "caller" |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_caller : M.IsAssociatedFunction Self "caller" caller.
  
  (*
      fn emit_event(&self, _event: Event) {
          unimplemented!()
      }
  *)
  Parameter emit_event : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_emit_event : M.IsAssociatedFunction Self "emit_event" emit_event.
End Impl_erc721_Env.

Module Impl_erc721_Erc721.
  Definition Self : Ty.t := Ty.path "erc721::Erc721".
  
  (*
      fn init_env() -> Env {
          unimplemented!()
      }
  *)
  Parameter init_env : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_init_env : M.IsAssociatedFunction Self "init_env" init_env.
  
  (*
      fn env(&self) -> Env {
          Self::init_env()
      }
  *)
  Definition env (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "erc721::Erc721", "init_env", [] |),
          []
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_env : M.IsAssociatedFunction Self "env" env.
  
  (*
      pub fn new() -> Self {
          Default::default()
      }
  *)
  Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_trait_method (|
            "core::default::Default",
            Ty.path "erc721::Erc721",
            [],
            "default",
            []
          |),
          []
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  
  (*
      fn balance_of_or_zero(&self, of: &AccountId) -> u32 {
          self.owned_tokens_count.get(of).unwrap_or(0 as u32)
      }
  *)
  Definition balance_of_or_zero (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; of ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let of := M.alloc (| of |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u32" ],
            "unwrap_or",
            []
          |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "erc721::Mapping")
                  []
                  [ Ty.path "erc721::AccountId"; Ty.path "u32" ],
                "get",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "erc721::Erc721",
                  "owned_tokens_count"
                |);
                M.read (| of |)
              ]
            |);
            M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U32 0 |)) |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_balance_of_or_zero :
    M.IsAssociatedFunction Self "balance_of_or_zero" balance_of_or_zero.
  
  (*
      fn clear_approval(&mut self, id: TokenId) {
          self.token_approvals.remove(id);
      }
  *)
  Definition clear_approval (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let id := M.alloc (| id |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "erc721::Mapping")
                    []
                    [ Ty.path "u32"; Ty.path "erc721::AccountId" ],
                  "remove",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "erc721::Erc721",
                    "token_approvals"
                  |);
                  M.read (| id |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_clear_approval :
    M.IsAssociatedFunction Self "clear_approval" clear_approval.
  
  (*
      fn approved_for_all(&self, owner: AccountId, operator: AccountId) -> bool {
          self.operator_approvals.contains(&(owner, operator))
      }
  *)
  Definition approved_for_all (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner; operator ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        let operator := M.alloc (| operator |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "erc721::Mapping")
              []
              [ Ty.tuple [ Ty.path "erc721::AccountId"; Ty.path "erc721::AccountId" ]; Ty.tuple []
              ],
            "contains",
            []
          |),
          [
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "erc721::Erc721",
              "operator_approvals"
            |);
            M.alloc (| Value.Tuple [ M.read (| owner |); M.read (| operator |) ] |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_approved_for_all :
    M.IsAssociatedFunction Self "approved_for_all" approved_for_all.
  
  (*
      pub fn owner_of(&self, id: TokenId) -> Option<AccountId> {
          self.token_owner.get(&id)
      }
  *)
  Definition owner_of (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let id := M.alloc (| id |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "erc721::Mapping") [] [ Ty.path "u32"; Ty.path "erc721::AccountId" ],
            "get",
            []
          |),
          [
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "erc721::Erc721",
              "token_owner"
            |);
            id
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_owner_of : M.IsAssociatedFunction Self "owner_of" owner_of.
  
  (*
      fn approved_or_owner(&self, from: Option<AccountId>, id: TokenId) -> bool {
          let owner = self.owner_of(id);
          from != Some(AccountId::from([0x0; 32]))
              && (from == owner
                  || from == self.token_approvals.get(&id)
                  || self.approved_for_all(
                      owner.expect("Error with AccountId"),
                      from.expect("Error with AccountId"),
                  ))
      }
  *)
  Definition approved_or_owner (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; from; id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let from := M.alloc (| from |) in
        let id := M.alloc (| id |) in
        M.read (|
          let~ owner :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "erc721::Erc721", "owner_of", [] |),
                [ M.read (| self |); M.read (| id |) ]
              |)
            |) in
          M.alloc (|
            LogicalOp.and (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "erc721::AccountId" ],
                  [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "erc721::AccountId" ] ],
                  "ne",
                  []
                |),
                [
                  from;
                  M.alloc (|
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::convert::From",
                            Ty.path "erc721::AccountId",
                            [
                              Ty.apply
                                (Ty.path "array")
                                [ Value.Integer IntegerKind.Usize 32 ]
                                [ Ty.path "u8" ]
                            ],
                            "from",
                            []
                          |),
                          [
                            repeat (|
                              Value.Integer IntegerKind.U8 0,
                              Value.Integer IntegerKind.Usize 32
                            |)
                          ]
                        |)
                      ]
                  |)
                ]
              |),
              ltac:(M.monadic
                (LogicalOp.or (|
                  LogicalOp.or (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "erc721::AccountId" ],
                        [
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.path "erc721::AccountId" ]
                        ],
                        "eq",
                        []
                      |),
                      [ from; owner ]
                    |),
                    ltac:(M.monadic
                      (M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialEq",
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.path "erc721::AccountId" ],
                          [
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "erc721::AccountId" ]
                          ],
                          "eq",
                          []
                        |),
                        [
                          from;
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "erc721::Mapping")
                                  []
                                  [ Ty.path "u32"; Ty.path "erc721::AccountId" ],
                                "get",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "erc721::Erc721",
                                  "token_approvals"
                                |);
                                id
                              ]
                            |)
                          |)
                        ]
                      |)))
                  |),
                  ltac:(M.monadic
                    (M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "erc721::Erc721",
                        "approved_for_all",
                        []
                      |),
                      [
                        M.read (| self |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "erc721::AccountId" ],
                            "expect",
                            []
                          |),
                          [ M.read (| owner |); M.read (| Value.String "Error with AccountId" |) ]
                        |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "erc721::AccountId" ],
                            "expect",
                            []
                          |),
                          [ M.read (| from |); M.read (| Value.String "Error with AccountId" |) ]
                        |)
                      ]
                    |)))
                |)))
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_approved_or_owner :
    M.IsAssociatedFunction Self "approved_or_owner" approved_or_owner.
  
  (*
      fn exists(&self, id: TokenId) -> bool {
          self.token_owner.contains(&id)
      }
  *)
  Definition exists_ (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let id := M.alloc (| id |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "erc721::Mapping") [] [ Ty.path "u32"; Ty.path "erc721::AccountId" ],
            "contains",
            []
          |),
          [
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "erc721::Erc721",
              "token_owner"
            |);
            id
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_exists_ : M.IsAssociatedFunction Self "exists_" exists_.
  
  (*
      pub fn balance_of(&self, owner: AccountId) -> u32 {
          self.balance_of_or_zero(&owner)
      }
  *)
  Definition balance_of (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "erc721::Erc721", "balance_of_or_zero", [] |),
          [ M.read (| self |); owner ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_balance_of : M.IsAssociatedFunction Self "balance_of" balance_of.
  
  (*
      pub fn get_approved(&self, id: TokenId) -> Option<AccountId> {
          self.token_approvals.get(&id)
      }
  *)
  Definition get_approved (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let id := M.alloc (| id |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "erc721::Mapping") [] [ Ty.path "u32"; Ty.path "erc721::AccountId" ],
            "get",
            []
          |),
          [
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "erc721::Erc721",
              "token_approvals"
            |);
            id
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get_approved : M.IsAssociatedFunction Self "get_approved" get_approved.
  
  (*
      pub fn is_approved_for_all(&self, owner: AccountId, operator: AccountId) -> bool {
          self.approved_for_all(owner, operator)
      }
  *)
  Definition is_approved_for_all (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner; operator ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        let operator := M.alloc (| operator |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "erc721::Erc721", "approved_for_all", [] |),
          [ M.read (| self |); M.read (| owner |); M.read (| operator |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_is_approved_for_all :
    M.IsAssociatedFunction Self "is_approved_for_all" is_approved_for_all.
  
  (*
      fn approve_for_all(&mut self, to: AccountId, approved: bool) -> Result<(), Error> {
          let caller = self.env().caller();
          if to == caller {
              return Err(Error::NotAllowed);
          }
          self.env().emit_event(Event::ApprovalForAll(ApprovalForAll {
              owner: caller,
              operator: to,
              approved,
          }));
  
          if approved {
              self.operator_approvals.insert((caller, to), ());
          } else {
              self.operator_approvals.remove((caller, to));
          }
  
          Ok(())
      }
  *)
  Definition approve_for_all (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; to; approved ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let to := M.alloc (| to |) in
        let approved := M.alloc (| approved |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ caller :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc721::Env", "caller", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc721::Erc721", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.path "erc721::AccountId",
                                  [ Ty.path "erc721::AccountId" ],
                                  "eq",
                                  []
                                |),
                                [ to; caller ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [ Value.StructTuple "erc721::Error::NotAllowed" [] ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc721::Env", "emit_event", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc721::Erc721", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |);
                      Value.StructTuple
                        "erc721::Event::ApprovalForAll"
                        [
                          Value.StructRecord
                            "erc721::ApprovalForAll"
                            [
                              ("owner", M.read (| caller |));
                              ("operator", M.read (| to |));
                              ("approved", M.read (| approved |))
                            ]
                        ]
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.use approved in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "erc721::Mapping")
                                  []
                                  [
                                    Ty.tuple
                                      [ Ty.path "erc721::AccountId"; Ty.path "erc721::AccountId" ];
                                    Ty.tuple []
                                  ],
                                "insert",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "erc721::Erc721",
                                  "operator_approvals"
                                |);
                                Value.Tuple [ M.read (| caller |); M.read (| to |) ];
                                Value.Tuple []
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "erc721::Mapping")
                                  []
                                  [
                                    Ty.tuple
                                      [ Ty.path "erc721::AccountId"; Ty.path "erc721::AccountId" ];
                                    Ty.tuple []
                                  ],
                                "remove",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "erc721::Erc721",
                                  "operator_approvals"
                                |);
                                Value.Tuple [ M.read (| caller |); M.read (| to |) ]
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_approve_for_all :
    M.IsAssociatedFunction Self "approve_for_all" approve_for_all.
  
  (*
      pub fn set_approval_for_all(&mut self, to: AccountId, approved: bool) -> Result<(), Error> {
          self.approve_for_all(to, approved)?;
          Ok(())
      }
  *)
  Definition set_approval_for_all (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; to; approved ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let to := M.alloc (| to |) in
        let approved := M.alloc (| approved |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [ Ty.tuple []; Ty.path "erc721::Error" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "erc721::Erc721",
                            "approve_for_all",
                            []
                          |),
                          [ M.read (| self |); M.read (| to |); M.read (| approved |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "erc721::Error" ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "core::convert::Infallible";
                                          Ty.path "erc721::Error"
                                        ]
                                    ],
                                    "from_residual",
                                    []
                                  |),
                                  [ M.read (| residual |) ]
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        val))
                  ]
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_set_approval_for_all :
    M.IsAssociatedFunction Self "set_approval_for_all" set_approval_for_all.
  
  (*
      fn approve_for(&mut self, to: &AccountId, id: TokenId) -> Result<(), Error> {
          let caller = self.env().caller();
          let owner = self.owner_of(id);
          if !(owner == Some(caller)
              || self.approved_for_all(owner.expect("Error with AccountId"), caller))
          {
              return Err(Error::NotAllowed);
          };
  
          if *to == AccountId::from([0x0; 32]) {
              return Err(Error::NotAllowed);
          };
  
          if self.token_approvals.contains(&id) {
              return Err(Error::CannotInsert);
          } else {
              self.token_approvals.insert(id, *to);
          }
  
          self.env().emit_event(Event::Approval(Approval {
              from: caller,
              to: *to,
              id,
          }));
  
          Ok(())
      }
  *)
  Definition approve_for (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; to; id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let to := M.alloc (| to |) in
        let id := M.alloc (| id |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ caller :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc721::Env", "caller", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc721::Erc721", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ owner :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc721::Erc721", "owner_of", [] |),
                    [ M.read (| self |); M.read (| id |) ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                LogicalOp.or (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "erc721::AccountId" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [ Ty.path "erc721::AccountId" ]
                                      ],
                                      "eq",
                                      []
                                    |),
                                    [
                                      owner;
                                      M.alloc (|
                                        Value.StructTuple
                                          "core::option::Option::Some"
                                          [ M.read (| caller |) ]
                                      |)
                                    ]
                                  |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "erc721::Erc721",
                                        "approved_for_all",
                                        []
                                      |),
                                      [
                                        M.read (| self |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "erc721::AccountId" ],
                                            "expect",
                                            []
                                          |),
                                          [
                                            M.read (| owner |);
                                            M.read (| Value.String "Error with AccountId" |)
                                          ]
                                        |);
                                        M.read (| caller |)
                                      ]
                                    |)))
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [ Value.StructTuple "erc721::Error::NotAllowed" [] ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.path "erc721::AccountId",
                                  [ Ty.path "erc721::AccountId" ],
                                  "eq",
                                  []
                                |),
                                [
                                  M.read (| to |);
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::From",
                                        Ty.path "erc721::AccountId",
                                        [
                                          Ty.apply
                                            (Ty.path "array")
                                            [ Value.Integer IntegerKind.Usize 32 ]
                                            [ Ty.path "u8" ]
                                        ],
                                        "from",
                                        []
                                      |),
                                      [
                                        repeat (|
                                          Value.Integer IntegerKind.U8 0,
                                          Value.Integer IntegerKind.Usize 32
                                        |)
                                      ]
                                    |)
                                  |)
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [ Value.StructTuple "erc721::Error::NotAllowed" [] ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "erc721::Mapping")
                                    []
                                    [ Ty.path "u32"; Ty.path "erc721::AccountId" ],
                                  "contains",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "erc721::Erc721",
                                    "token_approvals"
                                  |);
                                  id
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [ Value.StructTuple "erc721::Error::CannotInsert" [] ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "erc721::Mapping")
                                  []
                                  [ Ty.path "u32"; Ty.path "erc721::AccountId" ],
                                "insert",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "erc721::Erc721",
                                  "token_approvals"
                                |);
                                M.read (| id |);
                                M.read (| M.read (| to |) |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc721::Env", "emit_event", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc721::Erc721", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |);
                      Value.StructTuple
                        "erc721::Event::Approval"
                        [
                          Value.StructRecord
                            "erc721::Approval"
                            [
                              ("from", M.read (| caller |));
                              ("to", M.read (| M.read (| to |) |));
                              ("id", M.read (| id |))
                            ]
                        ]
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_approve_for : M.IsAssociatedFunction Self "approve_for" approve_for.
  
  (*
      pub fn approve(&mut self, to: AccountId, id: TokenId) -> Result<(), Error> {
          self.approve_for(&to, id)?;
          Ok(())
      }
  *)
  Definition approve (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; to; id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let to := M.alloc (| to |) in
        let id := M.alloc (| id |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [ Ty.tuple []; Ty.path "erc721::Error" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "erc721::Erc721",
                            "approve_for",
                            []
                          |),
                          [ M.read (| self |); to; M.read (| id |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "erc721::Error" ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "core::convert::Infallible";
                                          Ty.path "erc721::Error"
                                        ]
                                    ],
                                    "from_residual",
                                    []
                                  |),
                                  [ M.read (| residual |) ]
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        val))
                  ]
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_approve : M.IsAssociatedFunction Self "approve" approve.
  
  (*
      fn remove_token_from(&mut self, from: &AccountId, id: TokenId) -> Result<(), Error> {
          let Self {
              token_owner,
              owned_tokens_count,
              ..
          } = self;
  
          if !token_owner.contains(&id) {
              return Err(Error::TokenNotFound);
          }
  
          let count = owned_tokens_count
              .get(from)
              .map(|c| c - (1 as u32))
              .ok_or(Error::CannotFetchValue)?;
          owned_tokens_count.insert( *from, count);
          token_owner.remove(id);
  
          Ok(())
      }
  *)
  Definition remove_token_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; from; id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let from := M.alloc (| from |) in
        let id := M.alloc (| id |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "erc721::Erc721",
                          "token_owner"
                        |) in
                      let γ1_1 :=
                        M.SubPointer.get_struct_record_field (|
                          γ,
                          "erc721::Erc721",
                          "owned_tokens_count"
                        |) in
                      let token_owner := M.alloc (| γ1_0 |) in
                      let owned_tokens_count := M.alloc (| γ1_1 |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "erc721::Mapping")
                                              []
                                              [ Ty.path "u32"; Ty.path "erc721::AccountId" ],
                                            "contains",
                                            []
                                          |),
                                          [ M.read (| token_owner |); id ]
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        Value.StructTuple
                                          "core::result::Result::Err"
                                          [ Value.StructTuple "erc721::Error::TokenNotFound" [] ]
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ count :=
                        M.copy (|
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::try_trait::Try",
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [ Ty.path "u32"; Ty.path "erc721::Error" ],
                                  [],
                                  "branch",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "u32" ],
                                      "ok_or",
                                      [ Ty.path "erc721::Error" ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.path "u32" ],
                                          "map",
                                          [
                                            Ty.path "u32";
                                            Ty.function
                                              [ Ty.tuple [ Ty.path "u32" ] ]
                                              (Ty.path "u32")
                                          ]
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "erc721::Mapping")
                                                []
                                                [ Ty.path "erc721::AccountId"; Ty.path "u32" ],
                                              "get",
                                              []
                                            |),
                                            [ M.read (| owned_tokens_count |); M.read (| from |) ]
                                          |);
                                          M.closure
                                            (fun γ =>
                                              ltac:(M.monadic
                                                match γ with
                                                | [ α0 ] =>
                                                  ltac:(M.monadic
                                                    (M.match_operator (|
                                                      M.alloc (| α0 |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let c := M.copy (| γ |) in
                                                            BinOp.Wrap.sub (|
                                                              M.read (| c |),
                                                              M.read (|
                                                                M.use
                                                                  (M.alloc (|
                                                                    Value.Integer IntegerKind.U32 1
                                                                  |))
                                                              |)
                                                            |)))
                                                      ]
                                                    |)))
                                                | _ => M.impossible "wrong number of arguments"
                                                end))
                                        ]
                                      |);
                                      Value.StructTuple "erc721::Error::CannotFetchValue" []
                                    ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::ops::control_flow::ControlFlow::Break",
                                      0
                                    |) in
                                  let residual := M.copy (| γ0_0 |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::try_trait::FromResidual",
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                []
                                                [ Ty.tuple []; Ty.path "erc721::Error" ],
                                              [
                                                Ty.apply
                                                  (Ty.path "core::result::Result")
                                                  []
                                                  [
                                                    Ty.path "core::convert::Infallible";
                                                    Ty.path "erc721::Error"
                                                  ]
                                              ],
                                              "from_residual",
                                              []
                                            |),
                                            [ M.read (| residual |) ]
                                          |)
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::ops::control_flow::ControlFlow::Continue",
                                      0
                                    |) in
                                  let val := M.copy (| γ0_0 |) in
                                  val))
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "erc721::Mapping")
                                []
                                [ Ty.path "erc721::AccountId"; Ty.path "u32" ],
                              "insert",
                              []
                            |),
                            [
                              M.read (| owned_tokens_count |);
                              M.read (| M.read (| from |) |);
                              M.read (| count |)
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "erc721::Mapping")
                                []
                                [ Ty.path "u32"; Ty.path "erc721::AccountId" ],
                              "remove",
                              []
                            |),
                            [ M.read (| token_owner |); M.read (| id |) ]
                          |)
                        |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                      |)))
                ]
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_remove_token_from :
    M.IsAssociatedFunction Self "remove_token_from" remove_token_from.
  
  (*
      fn add_token_to(&mut self, to: &AccountId, id: TokenId) -> Result<(), Error> {
          let Self {
              token_owner,
              owned_tokens_count,
              ..
          } = self;
  
          if token_owner.contains(&id) {
              return Err(Error::TokenExists);
          }
  
          if *to == AccountId::from([0x0; 32]) {
              return Err(Error::NotAllowed);
          };
  
          let count = owned_tokens_count
              .get(to)
              .map(|c| c + (1 as u32))
              .unwrap_or(1);
  
          owned_tokens_count.insert( *to, count);
          token_owner.insert(id, *to);
  
          Ok(())
      }
  *)
  Parameter add_token_to : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_add_token_to : M.IsAssociatedFunction Self "add_token_to" add_token_to.
  
  (*
      fn transfer_token_from(
          &mut self,
          from: &AccountId,
          to: &AccountId,
          id: TokenId,
      ) -> Result<(), Error> {
          let caller = self.env().caller();
          if !self.exists(id) {
              return Err(Error::TokenNotFound);
          };
          if !self.approved_or_owner(Some(caller), id) {
              return Err(Error::NotApproved);
          };
          self.clear_approval(id);
          self.remove_token_from(from, id)?;
          self.add_token_to(to, id)?;
          self.env().emit_event(Event::Transfer(Transfer {
              from: Some( *from),
              to: Some( *to),
              id,
          }));
          Ok(())
      }
  *)
  Parameter transfer_token_from : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_transfer_token_from :
    M.IsAssociatedFunction Self "transfer_token_from" transfer_token_from.
  
  (*
      pub fn transfer(&mut self, destination: AccountId, id: TokenId) -> Result<(), Error> {
          let caller = self.env().caller();
          self.transfer_token_from(&caller, &destination, id)?;
          Ok(())
      }
  *)
  Definition transfer (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; destination; id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let destination := M.alloc (| destination |) in
        let id := M.alloc (| id |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ caller :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc721::Env", "caller", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc721::Erc721", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [ Ty.tuple []; Ty.path "erc721::Error" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "erc721::Erc721",
                            "transfer_token_from",
                            []
                          |),
                          [ M.read (| self |); caller; destination; M.read (| id |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "erc721::Error" ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "core::convert::Infallible";
                                          Ty.path "erc721::Error"
                                        ]
                                    ],
                                    "from_residual",
                                    []
                                  |),
                                  [ M.read (| residual |) ]
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        val))
                  ]
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_transfer : M.IsAssociatedFunction Self "transfer" transfer.
  
  (*
      pub fn transfer_from(
          &mut self,
          from: AccountId,
          to: AccountId,
          id: TokenId,
      ) -> Result<(), Error> {
          self.transfer_token_from(&from, &to, id)?;
          Ok(())
      }
  *)
  Definition transfer_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; from; to; id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let from := M.alloc (| from |) in
        let to := M.alloc (| to |) in
        let id := M.alloc (| id |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [ Ty.tuple []; Ty.path "erc721::Error" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "erc721::Erc721",
                            "transfer_token_from",
                            []
                          |),
                          [ M.read (| self |); from; to; M.read (| id |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "erc721::Error" ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "core::convert::Infallible";
                                          Ty.path "erc721::Error"
                                        ]
                                    ],
                                    "from_residual",
                                    []
                                  |),
                                  [ M.read (| residual |) ]
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        val))
                  ]
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_transfer_from :
    M.IsAssociatedFunction Self "transfer_from" transfer_from.
  
  (*
      pub fn mint(&mut self, id: TokenId) -> Result<(), Error> {
          let caller = self.env().caller();
          self.add_token_to(&caller, id)?;
          self.env().emit_event(Event::Transfer(Transfer {
              from: Some(AccountId::from([0x0; 32])),
              to: Some(caller),
              id,
          }));
          Ok(())
      }
  *)
  Definition mint (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let id := M.alloc (| id |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ caller :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc721::Env", "caller", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc721::Erc721", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [ Ty.tuple []; Ty.path "erc721::Error" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "erc721::Erc721",
                            "add_token_to",
                            []
                          |),
                          [ M.read (| self |); caller; M.read (| id |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "erc721::Error" ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "core::convert::Infallible";
                                          Ty.path "erc721::Error"
                                        ]
                                    ],
                                    "from_residual",
                                    []
                                  |),
                                  [ M.read (| residual |) ]
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        val))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "erc721::Env", "emit_event", [] |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "erc721::Erc721", "env", [] |),
                          [ M.read (| self |) ]
                        |)
                      |);
                      Value.StructTuple
                        "erc721::Event::Transfer"
                        [
                          Value.StructRecord
                            "erc721::Transfer"
                            [
                              ("from",
                                Value.StructTuple
                                  "core::option::Option::Some"
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::From",
                                        Ty.path "erc721::AccountId",
                                        [
                                          Ty.apply
                                            (Ty.path "array")
                                            [ Value.Integer IntegerKind.Usize 32 ]
                                            [ Ty.path "u8" ]
                                        ],
                                        "from",
                                        []
                                      |),
                                      [
                                        repeat (|
                                          Value.Integer IntegerKind.U8 0,
                                          Value.Integer IntegerKind.Usize 32
                                        |)
                                      ]
                                    |)
                                  ]);
                              ("to",
                                Value.StructTuple
                                  "core::option::Option::Some"
                                  [ M.read (| caller |) ]);
                              ("id", M.read (| id |))
                            ]
                        ]
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_mint : M.IsAssociatedFunction Self "mint" mint.
  
  (*
      pub fn burn(&mut self, id: TokenId) -> Result<(), Error> {
          let caller = self.env().caller();
          let Self {
              token_owner,
              owned_tokens_count,
              ..
          } = self;
  
          let owner = token_owner.get(&id).ok_or(Error::TokenNotFound)?;
          if owner != caller {
              return Err(Error::NotOwner);
          };
  
          let count = owned_tokens_count
              .get(&caller)
              .map(|c| c - 1)
              .ok_or(Error::CannotFetchValue)?;
          owned_tokens_count.insert(caller, count);
          token_owner.remove(id);
  
          self.env().emit_event(Event::Transfer(Transfer {
              from: Some(caller),
              to: Some(AccountId::from([0x0; 32])),
              id,
          }));
  
          Ok(())
      }
  *)
  Parameter burn : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_burn : M.IsAssociatedFunction Self "burn" burn.
End Impl_erc721_Erc721.
