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

Module marker.
  (* Trait *)
  (* Empty module 'Send' *)
  
  Module Impl_core_marker_Send_where_core_marker_Sized_T_for_pointer_const_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Send"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Send_where_core_marker_Sized_T_for_pointer_const_T.
  
  Module Impl_core_marker_Send_where_core_marker_Sized_T_for_pointer_mut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*mut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Send"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Send_where_core_marker_Sized_T_for_pointer_mut_T.
  
  Module Impl_core_marker_Send_where_core_marker_Sync_T_where_core_marker_Sized_T_for_ref__T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Send"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Send_where_core_marker_Sync_T_where_core_marker_Sized_T_for_ref__T.
  
  (* Trait *)
  (* Empty module 'Sized' *)
  
  (* Trait *)
  (* Empty module 'Unsize' *)
  
  (* Trait *)
  (* Empty module 'StructuralPartialEq' *)
  
  Module Impl_core_marker_StructuralPartialEq_for_usize.
    Definition Self : Ty.t := Ty.path "usize".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_usize.
  
  Module Impl_core_marker_StructuralPartialEq_for_u8.
    Definition Self : Ty.t := Ty.path "u8".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_u8.
  
  Module Impl_core_marker_StructuralPartialEq_for_u16.
    Definition Self : Ty.t := Ty.path "u16".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_u16.
  
  Module Impl_core_marker_StructuralPartialEq_for_u32.
    Definition Self : Ty.t := Ty.path "u32".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_u32.
  
  Module Impl_core_marker_StructuralPartialEq_for_u64.
    Definition Self : Ty.t := Ty.path "u64".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_u64.
  
  Module Impl_core_marker_StructuralPartialEq_for_u128.
    Definition Self : Ty.t := Ty.path "u128".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_u128.
  
  Module Impl_core_marker_StructuralPartialEq_for_isize.
    Definition Self : Ty.t := Ty.path "isize".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_isize.
  
  Module Impl_core_marker_StructuralPartialEq_for_i8.
    Definition Self : Ty.t := Ty.path "i8".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_i8.
  
  Module Impl_core_marker_StructuralPartialEq_for_i16.
    Definition Self : Ty.t := Ty.path "i16".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_i16.
  
  Module Impl_core_marker_StructuralPartialEq_for_i32.
    Definition Self : Ty.t := Ty.path "i32".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_i32.
  
  Module Impl_core_marker_StructuralPartialEq_for_i64.
    Definition Self : Ty.t := Ty.path "i64".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_i64.
  
  Module Impl_core_marker_StructuralPartialEq_for_i128.
    Definition Self : Ty.t := Ty.path "i128".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_i128.
  
  Module Impl_core_marker_StructuralPartialEq_for_bool.
    Definition Self : Ty.t := Ty.path "bool".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_bool.
  
  Module Impl_core_marker_StructuralPartialEq_for_char.
    Definition Self : Ty.t := Ty.path "char".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_char.
  
  Module Impl_core_marker_StructuralPartialEq_for_str.
    Definition Self : Ty.t := Ty.path "str".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_str.
  
  Module Impl_core_marker_StructuralPartialEq_for_Tuple_.
    Definition Self : Ty.t := Ty.tuple [].
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_Tuple_.
  
  Module Impl_core_marker_StructuralPartialEq_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        (Self N T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_array_N_T.
  
  Module Impl_core_marker_StructuralPartialEq_for_slice_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_slice_T.
  
  Module Impl_core_marker_StructuralPartialEq_where_core_marker_Sized_T_for_ref__T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_where_core_marker_Sized_T_for_ref__T.
  
  (* Trait *)
  (* Empty module 'Copy' *)
  
  Module Impl_core_marker_Copy_for_usize.
    Definition Self : Ty.t := Ty.path "usize".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_usize.
  
  Module Impl_core_marker_Copy_for_u8.
    Definition Self : Ty.t := Ty.path "u8".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_u8.
  
  Module Impl_core_marker_Copy_for_u16.
    Definition Self : Ty.t := Ty.path "u16".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_u16.
  
  Module Impl_core_marker_Copy_for_u32.
    Definition Self : Ty.t := Ty.path "u32".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_u32.
  
  Module Impl_core_marker_Copy_for_u64.
    Definition Self : Ty.t := Ty.path "u64".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_u64.
  
  Module Impl_core_marker_Copy_for_u128.
    Definition Self : Ty.t := Ty.path "u128".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_u128.
  
  Module Impl_core_marker_Copy_for_isize.
    Definition Self : Ty.t := Ty.path "isize".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_isize.
  
  Module Impl_core_marker_Copy_for_i8.
    Definition Self : Ty.t := Ty.path "i8".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_i8.
  
  Module Impl_core_marker_Copy_for_i16.
    Definition Self : Ty.t := Ty.path "i16".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_i16.
  
  Module Impl_core_marker_Copy_for_i32.
    Definition Self : Ty.t := Ty.path "i32".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_i32.
  
  Module Impl_core_marker_Copy_for_i64.
    Definition Self : Ty.t := Ty.path "i64".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_i64.
  
  Module Impl_core_marker_Copy_for_i128.
    Definition Self : Ty.t := Ty.path "i128".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_i128.
  
  Module Impl_core_marker_Copy_for_f16.
    Definition Self : Ty.t := Ty.path "f16".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_f16.
  
  Module Impl_core_marker_Copy_for_f32.
    Definition Self : Ty.t := Ty.path "f32".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_f32.
  
  Module Impl_core_marker_Copy_for_f64.
    Definition Self : Ty.t := Ty.path "f64".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_f64.
  
  Module Impl_core_marker_Copy_for_f128.
    Definition Self : Ty.t := Ty.path "f128".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_f128.
  
  Module Impl_core_marker_Copy_for_bool.
    Definition Self : Ty.t := Ty.path "bool".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_bool.
  
  Module Impl_core_marker_Copy_for_char.
    Definition Self : Ty.t := Ty.path "char".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_char.
  
  Module Impl_core_marker_Copy_where_core_marker_Sized_T_for_pointer_const_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_where_core_marker_Sized_T_for_pointer_const_T.
  
  Module Impl_core_marker_Copy_where_core_marker_Sized_T_for_pointer_mut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*mut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_where_core_marker_Sized_T_for_pointer_mut_T.
  
  Module Impl_core_marker_Copy_for_never.
    Definition Self : Ty.t := Ty.path "never".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_never.
  
  Module Impl_core_marker_Copy_where_core_marker_Sized_T_for_ref__T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_where_core_marker_Sized_T_for_ref__T.
  
  (* Trait *)
  (* Empty module 'Sync' *)
  
  Module Impl_core_marker_Sync_where_core_marker_Sized_T_for_pointer_const_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Sync"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Sync_where_core_marker_Sized_T_for_pointer_const_T.
  
  Module Impl_core_marker_Sync_where_core_marker_Sized_T_for_pointer_mut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*mut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Sync"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Sync_where_core_marker_Sized_T_for_pointer_mut_T.
  
  (* StructTuple
    {
      name := "PhantomData";
      const_params := [];
      ty_params := [ "T" ];
      fields := [];
    } *)
  
  Module Impl_core_hash_Hash_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ].
    
    (*     fn hash<H: Hasher>(&self, _: &mut H) {} *)
    Definition hash (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ H ], [ self; β1 ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let β1 := M.alloc (| β1 |) in
          M.match_operator (| β1, [ fun γ => ltac:(M.monadic (Value.Tuple [])) ] |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::hash::Hash"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method (hash T)) ].
  End Impl_core_hash_Hash_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
  
  Module Impl_core_cmp_PartialEq_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ].
    
    (*
        fn eq(&self, _other: &PhantomData<T>) -> bool {
            true
        }
    *)
    Definition eq (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; _other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let _other := M.alloc (| _other |) in
          Value.Bool true))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialEq"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method (eq T)) ].
  End Impl_core_cmp_PartialEq_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
  
  Module Impl_core_cmp_Eq_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance "core::cmp::Eq" (Self T) (* Trait polymorphic types *) [] (* Instance *) [].
  End Impl_core_cmp_Eq_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
  
  Module Impl_core_cmp_PartialOrd_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ].
    
    (*
        fn partial_cmp(&self, _other: &PhantomData<T>) -> Option<cmp::Ordering> {
            Option::Some(cmp::Ordering::Equal)
        }
    *)
    Definition partial_cmp (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; _other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let _other := M.alloc (| _other |) in
          Value.StructTuple
            "core::option::Option::Some"
            [ Value.StructTuple "core::cmp::Ordering::Equal" [] ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method (partial_cmp T)) ].
  End Impl_core_cmp_PartialOrd_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
  
  Module Impl_core_cmp_Ord_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ].
    
    (*
        fn cmp(&self, _other: &PhantomData<T>) -> cmp::Ordering {
            cmp::Ordering::Equal
        }
    *)
    Definition cmp (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; _other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let _other := M.alloc (| _other |) in
          Value.StructTuple "core::cmp::Ordering::Equal" []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::Ord"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method (cmp T)) ].
  End Impl_core_cmp_Ord_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
  
  Module Impl_core_marker_Copy_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
  
  Module Impl_core_clone_Clone_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ].
    
    (*
        fn clone(&self) -> Self {
            Self
        }
    *)
    Definition clone (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| (* Expected a function name *) M.alloc (| Value.Tuple [] |) |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone T)) ].
  End Impl_core_clone_Clone_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
  
  Module Impl_core_default_Default_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ].
    
    (*
        fn default() -> Self {
            Self
        }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic (M.read (| (* Expected a function name *) M.alloc (| Value.Tuple [] |) |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
  End Impl_core_default_Default_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
  
  Module Impl_core_marker_StructuralPartialEq_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
  
  (* Trait *)
  (* Empty module 'DiscriminantKind' *)
  
  (* Trait *)
  (* Empty module 'Freeze' *)
  
  Module Impl_core_marker_Freeze_where_core_marker_Sized_T_for_core_cell_UnsafeCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Freeze"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Freeze_where_core_marker_Sized_T_for_core_cell_UnsafeCell_T.
  
  Module Impl_core_marker_Freeze_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Freeze"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Freeze_where_core_marker_Sized_T_for_core_marker_PhantomData_T.
  
  Module Impl_core_marker_Freeze_where_core_marker_Sized_T_for_pointer_const_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Freeze"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Freeze_where_core_marker_Sized_T_for_pointer_const_T.
  
  Module Impl_core_marker_Freeze_where_core_marker_Sized_T_for_pointer_mut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*mut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Freeze"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Freeze_where_core_marker_Sized_T_for_pointer_mut_T.
  
  Module Impl_core_marker_Freeze_where_core_marker_Sized_T_for_ref__T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Freeze"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Freeze_where_core_marker_Sized_T_for_ref__T.
  
  Module Impl_core_marker_Freeze_where_core_marker_Sized_T_for_ref_mut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Freeze"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Freeze_where_core_marker_Sized_T_for_ref_mut_T.
  
  (* Trait *)
  (* Empty module 'Unpin' *)
  
  (* StructTuple
    {
      name := "PhantomPinned";
      const_params := [];
      ty_params := [];
      fields := [];
    } *)
  
  Module Impl_core_fmt_Debug_for_core_marker_PhantomPinned.
    Definition Self : Ty.t := Ty.path "core::marker::PhantomPinned".
    
    (* 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 (| Value.String "PhantomPinned" |) ]
          |)))
      | _, _, _ => 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_core_marker_PhantomPinned.
  
  Module Impl_core_default_Default_for_core_marker_PhantomPinned.
    Definition Self : Ty.t := Ty.path "core::marker::PhantomPinned".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] => ltac:(M.monadic (Value.StructTuple "core::marker::PhantomPinned" []))
      | _, _, _ => 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_core_marker_PhantomPinned.
  
  Module Impl_core_marker_Copy_for_core_marker_PhantomPinned.
    Definition Self : Ty.t := Ty.path "core::marker::PhantomPinned".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_core_marker_PhantomPinned.
  
  Module Impl_core_clone_Clone_for_core_marker_PhantomPinned.
    Definition Self : Ty.t := Ty.path "core::marker::PhantomPinned".
    
    (* 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_core_marker_PhantomPinned.
  
  Module Impl_core_cmp_Eq_for_core_marker_PhantomPinned.
    Definition Self : Ty.t := Ty.path "core::marker::PhantomPinned".
    
    (* 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_core_marker_PhantomPinned.
  
  Module Impl_core_marker_StructuralPartialEq_for_core_marker_PhantomPinned.
    Definition Self : Ty.t := Ty.path "core::marker::PhantomPinned".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_marker_PhantomPinned.
  
  Module Impl_core_cmp_PartialEq_for_core_marker_PhantomPinned.
    Definition Self : Ty.t := Ty.path "core::marker::PhantomPinned".
    
    (* 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
          Value.Bool true))
      | _, _, _ => 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_core_marker_PhantomPinned.
  
  Module Impl_core_cmp_Ord_for_core_marker_PhantomPinned.
    Definition Self : Ty.t := Ty.path "core::marker::PhantomPinned".
    
    (* 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
          Value.StructTuple "core::cmp::Ordering::Equal" []))
      | _, _, _ => 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_core_marker_PhantomPinned.
  
  Module Impl_core_cmp_PartialOrd_for_core_marker_PhantomPinned.
    Definition Self : Ty.t := Ty.path "core::marker::PhantomPinned".
    
    (* 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
          Value.StructTuple
            "core::option::Option::Some"
            [ Value.StructTuple "core::cmp::Ordering::Equal" [] ]))
      | _, _, _ => 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_core_marker_PhantomPinned.
  
  Module Impl_core_hash_Hash_for_core_marker_PhantomPinned.
    Definition Self : Ty.t := Ty.path "core::marker::PhantomPinned".
    
    (* 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
          Value.Tuple []))
      | _, _, _ => 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_core_marker_PhantomPinned.
  
  Module Impl_core_marker_Unpin_for_core_marker_PhantomPinned.
    Definition Self : Ty.t := Ty.path "core::marker::PhantomPinned".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Unpin"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Unpin_for_core_marker_PhantomPinned.
  
  Module Impl_core_marker_Unpin_where_core_marker_Sized_T_for_ref__T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Unpin"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Unpin_where_core_marker_Sized_T_for_ref__T.
  
  Module Impl_core_marker_Unpin_where_core_marker_Sized_T_for_ref_mut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Unpin"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Unpin_where_core_marker_Sized_T_for_ref_mut_T.
  
  Module Impl_core_marker_Unpin_where_core_marker_Sized_T_for_pointer_const_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Unpin"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Unpin_where_core_marker_Sized_T_for_pointer_const_T.
  
  Module Impl_core_marker_Unpin_where_core_marker_Sized_T_for_pointer_mut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*mut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Unpin"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Unpin_where_core_marker_Sized_T_for_pointer_mut_T.
  
  (* Trait *)
  (* Empty module 'Destruct' *)
  
  (* Trait *)
  (* Empty module 'Tuple' *)
  
  (* Trait *)
  (* Empty module 'PointerLike' *)
  
  (* Trait *)
  (* Empty module 'ConstParamTy_' *)
  
  (* Trait *)
  (* Empty module 'UnsizedConstParamTy' *)
  
  Module Impl_core_marker_ConstParamTy__for_usize.
    Definition Self : Ty.t := Ty.path "usize".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_usize.
  
  Module Impl_core_marker_ConstParamTy__for_u8.
    Definition Self : Ty.t := Ty.path "u8".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_u8.
  
  Module Impl_core_marker_ConstParamTy__for_u16.
    Definition Self : Ty.t := Ty.path "u16".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_u16.
  
  Module Impl_core_marker_ConstParamTy__for_u32.
    Definition Self : Ty.t := Ty.path "u32".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_u32.
  
  Module Impl_core_marker_ConstParamTy__for_u64.
    Definition Self : Ty.t := Ty.path "u64".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_u64.
  
  Module Impl_core_marker_ConstParamTy__for_u128.
    Definition Self : Ty.t := Ty.path "u128".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_u128.
  
  Module Impl_core_marker_ConstParamTy__for_isize.
    Definition Self : Ty.t := Ty.path "isize".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_isize.
  
  Module Impl_core_marker_ConstParamTy__for_i8.
    Definition Self : Ty.t := Ty.path "i8".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_i8.
  
  Module Impl_core_marker_ConstParamTy__for_i16.
    Definition Self : Ty.t := Ty.path "i16".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_i16.
  
  Module Impl_core_marker_ConstParamTy__for_i32.
    Definition Self : Ty.t := Ty.path "i32".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_i32.
  
  Module Impl_core_marker_ConstParamTy__for_i64.
    Definition Self : Ty.t := Ty.path "i64".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_i64.
  
  Module Impl_core_marker_ConstParamTy__for_i128.
    Definition Self : Ty.t := Ty.path "i128".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_i128.
  
  Module Impl_core_marker_ConstParamTy__for_bool.
    Definition Self : Ty.t := Ty.path "bool".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_bool.
  
  Module Impl_core_marker_ConstParamTy__for_char.
    Definition Self : Ty.t := Ty.path "char".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_char.
  
  Module Impl_core_marker_ConstParamTy__for_Tuple_.
    Definition Self : Ty.t := Ty.tuple [].
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__for_Tuple_.
  
  Module Impl_core_marker_ConstParamTy__where_core_marker_ConstParamTy__T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::marker::ConstParamTy_"
        (Self N T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_ConstParamTy__where_core_marker_ConstParamTy__T_for_array_N_T.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_usize.
    Definition Self : Ty.t := Ty.path "usize".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_usize.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_u8.
    Definition Self : Ty.t := Ty.path "u8".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_u8.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_u16.
    Definition Self : Ty.t := Ty.path "u16".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_u16.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_u32.
    Definition Self : Ty.t := Ty.path "u32".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_u32.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_u64.
    Definition Self : Ty.t := Ty.path "u64".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_u64.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_u128.
    Definition Self : Ty.t := Ty.path "u128".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_u128.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_isize.
    Definition Self : Ty.t := Ty.path "isize".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_isize.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_i8.
    Definition Self : Ty.t := Ty.path "i8".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_i8.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_i16.
    Definition Self : Ty.t := Ty.path "i16".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_i16.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_i32.
    Definition Self : Ty.t := Ty.path "i32".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_i32.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_i64.
    Definition Self : Ty.t := Ty.path "i64".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_i64.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_i128.
    Definition Self : Ty.t := Ty.path "i128".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_i128.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_bool.
    Definition Self : Ty.t := Ty.path "bool".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_bool.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_char.
    Definition Self : Ty.t := Ty.path "char".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_char.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_Tuple_.
    Definition Self : Ty.t := Ty.tuple [].
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_Tuple_.
  
  Module Impl_core_marker_UnsizedConstParamTy_where_core_marker_UnsizedConstParamTy_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        (Self N T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_where_core_marker_UnsizedConstParamTy_T_for_array_N_T.
  
  Module Impl_core_marker_UnsizedConstParamTy_for_str.
    Definition Self : Ty.t := Ty.path "str".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_for_str.
  
  Module Impl_core_marker_UnsizedConstParamTy_where_core_marker_UnsizedConstParamTy_T_for_slice_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_where_core_marker_UnsizedConstParamTy_T_for_slice_T.
  
  Module Impl_core_marker_UnsizedConstParamTy_where_core_marker_UnsizedConstParamTy_T_where_core_marker_Sized_T_for_ref__T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::UnsizedConstParamTy"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_UnsizedConstParamTy_where_core_marker_UnsizedConstParamTy_T_where_core_marker_Sized_T_for_ref__T.
  
  (* Trait *)
  (* Empty module 'FnPtr' *)
  
  Module effects.
    (* StructTuple
      {
        name := "NoRuntime";
        const_params := [];
        ty_params := [];
        fields := [];
      } *)
    
    (* StructTuple
      {
        name := "Maybe";
        const_params := [];
        ty_params := [];
        fields := [];
      } *)
    
    (* StructTuple
      {
        name := "Runtime";
        const_params := [];
        ty_params := [];
        fields := [];
      } *)
    
    (* Trait *)
    (* Empty module 'Compat' *)
    
    Module Impl_core_marker_effects_Compat_for_core_marker_effects_NoRuntime.
      Definition Self : Ty.t := Ty.path "core::marker::effects::NoRuntime".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::effects::Compat"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_effects_Compat_for_core_marker_effects_NoRuntime.
    
    Module Impl_core_marker_effects_Compat_for_core_marker_effects_Runtime.
      Definition Self : Ty.t := Ty.path "core::marker::effects::Runtime".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::effects::Compat"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_effects_Compat_for_core_marker_effects_Runtime.
    
    Module Impl_core_marker_effects_Compat_for_core_marker_effects_Maybe.
      Definition Self (RUNTIME : Value.t) : Ty.t := Ty.path "core::marker::effects::Maybe".
      
      Axiom Implements :
        forall (RUNTIME : Value.t),
        M.IsTraitInstance
          "core::marker::effects::Compat"
          (Self RUNTIME)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_effects_Compat_for_core_marker_effects_Maybe.
    
    (* Trait *)
    (* Empty module 'TyCompat' *)
    
    Module Impl_core_marker_effects_TyCompat_where_core_marker_Sized_T_T_for_T.
      Definition Self (T : Ty.t) : Ty.t := T.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::marker::effects::TyCompat"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) T ]
          (* Instance *) [].
    End Impl_core_marker_effects_TyCompat_where_core_marker_Sized_T_T_for_T.
    
    Module Impl_core_marker_effects_TyCompat_where_core_marker_Sized_T_core_marker_effects_Maybe_for_T.
      Definition Self (T : Ty.t) : Ty.t := T.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::marker::effects::TyCompat"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) Ty.path "core::marker::effects::Maybe" ]
          (* Instance *) [].
    End Impl_core_marker_effects_TyCompat_where_core_marker_Sized_T_core_marker_effects_Maybe_for_T.
    
    (* Trait *)
    (* Empty module 'Intersection' *)
    
    Module Impl_core_marker_effects_Intersection_for_Tuple_.
      Definition Self : Ty.t := Ty.tuple [].
      
      (*         type Output = Maybe; *)
      Definition _Output : Ty.t := Ty.path "core::marker::effects::Maybe".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::effects::Intersection"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("Output", InstanceField.Ty _Output) ].
    End Impl_core_marker_effects_Intersection_for_Tuple_.
  End effects.
End marker.
