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

(* StructTuple
  {
    name := "PhantomTuple";
    const_params := [];
    ty_params := [ "A"; "B" ];
    fields := [ A; Ty.apply (Ty.path "core::marker::PhantomData") [] [ B ] ];
  } *)

Module Impl_core_marker_StructuralPartialEq_for_generics_phantom_type_PhantomTuple_A_B.
  Definition Self (A B : Ty.t) : Ty.t :=
    Ty.apply (Ty.path "generics_phantom_type::PhantomTuple") [] [ A; B ].
  
  Axiom Implements :
    forall (A B : Ty.t),
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      (Self A B)
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_generics_phantom_type_PhantomTuple_A_B.

Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_A_where_core_cmp_PartialEq_B_for_generics_phantom_type_PhantomTuple_A_B.
  Definition Self (A B : Ty.t) : Ty.t :=
    Ty.apply (Ty.path "generics_phantom_type::PhantomTuple") [] [ A; B ].
  
  Parameter eq : forall (A B : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    forall (A B : Ty.t),
    M.IsTraitInstance
      "core::cmp::PartialEq"
      (Self A B)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("eq", InstanceField.Method (eq A B)) ].
End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_A_where_core_cmp_PartialEq_B_for_generics_phantom_type_PhantomTuple_A_B.

(* StructRecord
  {
    name := "PhantomStruct";
    const_params := [];
    ty_params := [ "A"; "B" ];
    fields :=
      [ ("first", A); ("phantom", Ty.apply (Ty.path "core::marker::PhantomData") [] [ B ]) ];
  } *)

Module Impl_core_marker_StructuralPartialEq_for_generics_phantom_type_PhantomStruct_A_B.
  Definition Self (A B : Ty.t) : Ty.t :=
    Ty.apply (Ty.path "generics_phantom_type::PhantomStruct") [] [ A; B ].
  
  Axiom Implements :
    forall (A B : Ty.t),
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      (Self A B)
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_generics_phantom_type_PhantomStruct_A_B.

Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_A_where_core_cmp_PartialEq_B_for_generics_phantom_type_PhantomStruct_A_B.
  Definition Self (A B : Ty.t) : Ty.t :=
    Ty.apply (Ty.path "generics_phantom_type::PhantomStruct") [] [ A; B ].
  
  Parameter eq : forall (A B : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    forall (A B : Ty.t),
    M.IsTraitInstance
      "core::cmp::PartialEq"
      (Self A B)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("eq", InstanceField.Method (eq A B)) ].
End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_A_where_core_cmp_PartialEq_B_for_generics_phantom_type_PhantomStruct_A_B.

Parameter main : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Axiom Function_main : M.IsFunction "generics_phantom_type::main" main.
