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

(*
Enum IndexKind
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "ModuleHandle";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "StructHandle";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "FunctionHandle";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "FieldHandle";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "FriendDeclaration";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "FunctionInstantiation";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "FieldInstantiation";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "StructDefinition";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "StructDefInstantiation";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "FunctionDefinition";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "FieldDefinition";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "Signature";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "Identifier";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "AddressIdentifier";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "ConstantPool";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "LocalPool";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "CodeDefinition";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "TypeParameter";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "MemberCount";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

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

Module Impl_core_clone_Clone_for_move_binary_format_IndexKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::IndexKind".
  
  (* 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_move_binary_format_IndexKind.

Module Impl_core_fmt_Debug_for_move_binary_format_IndexKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::IndexKind".
  
  (* Debug *)
  Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
          [
            M.read (| f |);
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::ModuleHandle" |) in
                      M.alloc (| M.read (| Value.String "ModuleHandle" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::StructHandle" |) in
                      M.alloc (| M.read (| Value.String "StructHandle" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::FunctionHandle"
                        |) in
                      M.alloc (| M.read (| Value.String "FunctionHandle" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::FieldHandle" |) in
                      M.alloc (| M.read (| Value.String "FieldHandle" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::FriendDeclaration"
                        |) in
                      M.alloc (| M.read (| Value.String "FriendDeclaration" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::FunctionInstantiation"
                        |) in
                      M.alloc (| M.read (| Value.String "FunctionInstantiation" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::FieldInstantiation"
                        |) in
                      M.alloc (| M.read (| Value.String "FieldInstantiation" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::StructDefinition"
                        |) in
                      M.alloc (| M.read (| Value.String "StructDefinition" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::StructDefInstantiation"
                        |) in
                      M.alloc (| M.read (| Value.String "StructDefInstantiation" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::FunctionDefinition"
                        |) in
                      M.alloc (| M.read (| Value.String "FunctionDefinition" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::FieldDefinition"
                        |) in
                      M.alloc (| M.read (| Value.String "FieldDefinition" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::Signature" |) in
                      M.alloc (| M.read (| Value.String "Signature" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::Identifier" |) in
                      M.alloc (| M.read (| Value.String "Identifier" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::AddressIdentifier"
                        |) in
                      M.alloc (| M.read (| Value.String "AddressIdentifier" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::ConstantPool" |) in
                      M.alloc (| M.read (| Value.String "ConstantPool" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::LocalPool" |) in
                      M.alloc (| M.read (| Value.String "LocalPool" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::CodeDefinition"
                        |) in
                      M.alloc (| M.read (| Value.String "CodeDefinition" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::TypeParameter" |) in
                      M.alloc (| M.read (| Value.String "TypeParameter" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::MemberCount" |) in
                      M.alloc (| M.read (| Value.String "MemberCount" |) |)))
                ]
              |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::fmt::Debug"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
End Impl_core_fmt_Debug_for_move_binary_format_IndexKind.

Module Impl_core_cmp_Eq_for_move_binary_format_IndexKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::IndexKind".
  
  (* 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_move_binary_format_IndexKind.

Module Impl_core_hash_Hash_for_move_binary_format_IndexKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::IndexKind".
  
  (* Hash *)
  Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ __H ], [ self; state ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let state := M.alloc (| state |) in
        M.read (|
          let~ __self_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_binary_format::IndexKind" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (| "core::hash::Hash", Ty.path "isize", [], "hash", [ __H ] |),
              [ __self_discr; M.read (| state |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::hash::Hash"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("hash", InstanceField.Method hash) ].
End Impl_core_hash_Hash_for_move_binary_format_IndexKind.

Module Impl_core_cmp_Ord_for_move_binary_format_IndexKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::IndexKind".
  
  (* Ord *)
  Definition cmp (ε : 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 "move_binary_format::IndexKind" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_binary_format::IndexKind" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (| "core::cmp::Ord", Ty.path "isize", [], "cmp", [] |),
              [ __self_discr; __arg1_discr ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Ord"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
End Impl_core_cmp_Ord_for_move_binary_format_IndexKind.

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

Module Impl_core_cmp_PartialEq_for_move_binary_format_IndexKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::IndexKind".
  
  (* 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 "move_binary_format::IndexKind" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_binary_format::IndexKind" ]
                |),
                [ 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_move_binary_format_IndexKind.

Module Impl_core_cmp_PartialOrd_for_move_binary_format_IndexKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::IndexKind".
  
  (* PartialOrd *)
  Definition partial_cmp (ε : 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 "move_binary_format::IndexKind" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_binary_format::IndexKind" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialOrd",
                Ty.path "isize",
                [ Ty.path "isize" ],
                "partial_cmp",
                []
              |),
              [ __self_discr; __arg1_discr ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialOrd"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
End Impl_core_cmp_PartialOrd_for_move_binary_format_IndexKind.

Module Impl_move_binary_format_IndexKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::IndexKind".
  
  (*
      pub fn variants() -> &'static [IndexKind] {
          use IndexKind::*;
  
          // XXX ensure this list stays up to date!
          &[
              ModuleHandle,
              StructHandle,
              FunctionHandle,
              FieldHandle,
              FriendDeclaration,
              StructDefInstantiation,
              FunctionInstantiation,
              FieldInstantiation,
              StructDefinition,
              FunctionDefinition,
              FieldDefinition,
              Signature,
              Identifier,
              ConstantPool,
              LocalPool,
              CodeDefinition,
              TypeParameter,
              MemberCount,
          ]
      }
  *)
  Definition variants (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.alloc (|
          Value.Array
            [
              Value.StructTuple "move_binary_format::IndexKind::ModuleHandle" [];
              Value.StructTuple "move_binary_format::IndexKind::StructHandle" [];
              Value.StructTuple "move_binary_format::IndexKind::FunctionHandle" [];
              Value.StructTuple "move_binary_format::IndexKind::FieldHandle" [];
              Value.StructTuple "move_binary_format::IndexKind::FriendDeclaration" [];
              Value.StructTuple "move_binary_format::IndexKind::StructDefInstantiation" [];
              Value.StructTuple "move_binary_format::IndexKind::FunctionInstantiation" [];
              Value.StructTuple "move_binary_format::IndexKind::FieldInstantiation" [];
              Value.StructTuple "move_binary_format::IndexKind::StructDefinition" [];
              Value.StructTuple "move_binary_format::IndexKind::FunctionDefinition" [];
              Value.StructTuple "move_binary_format::IndexKind::FieldDefinition" [];
              Value.StructTuple "move_binary_format::IndexKind::Signature" [];
              Value.StructTuple "move_binary_format::IndexKind::Identifier" [];
              Value.StructTuple "move_binary_format::IndexKind::ConstantPool" [];
              Value.StructTuple "move_binary_format::IndexKind::LocalPool" [];
              Value.StructTuple "move_binary_format::IndexKind::CodeDefinition" [];
              Value.StructTuple "move_binary_format::IndexKind::TypeParameter" [];
              Value.StructTuple "move_binary_format::IndexKind::MemberCount" []
            ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_variants : M.IsAssociatedFunction Self "variants" variants.
End Impl_move_binary_format_IndexKind.

Module Impl_core_fmt_Display_for_move_binary_format_IndexKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::IndexKind".
  
  (*
      fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
          use IndexKind::*;
  
          let desc = match self {
              ModuleHandle => "module handle",
              StructHandle => "struct handle",
              FunctionHandle => "function handle",
              FieldHandle => "field handle",
              FriendDeclaration => "friend declaration",
              StructDefInstantiation => "struct instantiation",
              FunctionInstantiation => "function instantiation",
              FieldInstantiation => "field instantiation",
              StructDefinition => "struct definition",
              FunctionDefinition => "function definition",
              FieldDefinition => "field definition",
              Signature => "signature",
              Identifier => "identifier",
              AddressIdentifier => "address identifier",
              ConstantPool => "constant pool",
              LocalPool => "local pool",
              CodeDefinition => "code definition pool",
              TypeParameter => "type parameter",
              MemberCount => "field offset",
          };
  
          f.write_str(desc)
      }
  *)
  Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.read (|
          let~ desc :=
            M.copy (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::ModuleHandle" |) in
                      Value.String "module handle"));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::StructHandle" |) in
                      M.alloc (| M.read (| Value.String "struct handle" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::FunctionHandle"
                        |) in
                      M.alloc (| M.read (| Value.String "function handle" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::FieldHandle" |) in
                      M.alloc (| M.read (| Value.String "field handle" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::FriendDeclaration"
                        |) in
                      M.alloc (| M.read (| Value.String "friend declaration" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::StructDefInstantiation"
                        |) in
                      M.alloc (| M.read (| Value.String "struct instantiation" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::FunctionInstantiation"
                        |) in
                      M.alloc (| M.read (| Value.String "function instantiation" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::FieldInstantiation"
                        |) in
                      M.alloc (| M.read (| Value.String "field instantiation" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::StructDefinition"
                        |) in
                      M.alloc (| M.read (| Value.String "struct definition" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::FunctionDefinition"
                        |) in
                      M.alloc (| M.read (| Value.String "function definition" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::FieldDefinition"
                        |) in
                      M.alloc (| M.read (| Value.String "field definition" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::Signature" |) in
                      M.alloc (| M.read (| Value.String "signature" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::Identifier" |) in
                      M.alloc (| M.read (| Value.String "identifier" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::AddressIdentifier"
                        |) in
                      M.alloc (| M.read (| Value.String "address identifier" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::ConstantPool" |) in
                      M.alloc (| M.read (| Value.String "constant pool" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::LocalPool" |) in
                      M.alloc (| M.read (| Value.String "local pool" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::IndexKind::CodeDefinition"
                        |) in
                      M.alloc (| M.read (| Value.String "code definition pool" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::TypeParameter" |) in
                      M.alloc (| M.read (| Value.String "type parameter" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_binary_format::IndexKind::MemberCount" |) in
                      M.alloc (| M.read (| Value.String "field offset" |) |)))
                ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
              [ M.read (| f |); M.read (| desc |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::fmt::Display"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
End Impl_core_fmt_Display_for_move_binary_format_IndexKind.

(*
Enum SignatureTokenKind
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Value";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "Reference";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "MutableReference";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

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

Module Impl_core_clone_Clone_for_move_binary_format_SignatureTokenKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::SignatureTokenKind".
  
  (* 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_move_binary_format_SignatureTokenKind.

Module Impl_core_fmt_Debug_for_move_binary_format_SignatureTokenKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::SignatureTokenKind".
  
  (* Debug *)
  Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
          [
            M.read (| f |);
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::SignatureTokenKind::Value"
                        |) in
                      M.alloc (| M.read (| Value.String "Value" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::SignatureTokenKind::Reference"
                        |) in
                      M.alloc (| M.read (| Value.String "Reference" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::SignatureTokenKind::MutableReference"
                        |) in
                      M.alloc (| M.read (| Value.String "MutableReference" |) |)))
                ]
              |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::fmt::Debug"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
End Impl_core_fmt_Debug_for_move_binary_format_SignatureTokenKind.

Module Impl_core_cmp_Eq_for_move_binary_format_SignatureTokenKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::SignatureTokenKind".
  
  (* 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_move_binary_format_SignatureTokenKind.

Module Impl_core_cmp_Ord_for_move_binary_format_SignatureTokenKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::SignatureTokenKind".
  
  (* Ord *)
  Definition cmp (ε : 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 "move_binary_format::SignatureTokenKind" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_binary_format::SignatureTokenKind" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (| "core::cmp::Ord", Ty.path "isize", [], "cmp", [] |),
              [ __self_discr; __arg1_discr ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Ord"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
End Impl_core_cmp_Ord_for_move_binary_format_SignatureTokenKind.

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

Module Impl_core_cmp_PartialEq_for_move_binary_format_SignatureTokenKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::SignatureTokenKind".
  
  (* 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 "move_binary_format::SignatureTokenKind" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_binary_format::SignatureTokenKind" ]
                |),
                [ 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_move_binary_format_SignatureTokenKind.

Module Impl_core_cmp_PartialOrd_for_move_binary_format_SignatureTokenKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::SignatureTokenKind".
  
  (* PartialOrd *)
  Definition partial_cmp (ε : 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 "move_binary_format::SignatureTokenKind" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_binary_format::SignatureTokenKind" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialOrd",
                Ty.path "isize",
                [ Ty.path "isize" ],
                "partial_cmp",
                []
              |),
              [ __self_discr; __arg1_discr ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialOrd"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
End Impl_core_cmp_PartialOrd_for_move_binary_format_SignatureTokenKind.

Module Impl_core_fmt_Display_for_move_binary_format_SignatureTokenKind.
  Definition Self : Ty.t := Ty.path "move_binary_format::SignatureTokenKind".
  
  (*
      fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
          use SignatureTokenKind::*;
  
          let desc = match self {
              Value => "value",
              Reference => "reference",
              MutableReference => "mutable reference",
          };
  
          f.write_str(desc)
      }
  *)
  Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.read (|
          let~ desc :=
            M.copy (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::SignatureTokenKind::Value"
                        |) in
                      Value.String "value"));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::SignatureTokenKind::Reference"
                        |) in
                      M.alloc (| M.read (| Value.String "reference" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::SignatureTokenKind::MutableReference"
                        |) in
                      M.alloc (| M.read (| Value.String "mutable reference" |) |)))
                ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
              [ M.read (| f |); M.read (| desc |) ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::fmt::Display"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
End Impl_core_fmt_Display_for_move_binary_format_SignatureTokenKind.
