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

Module mem.
  Module manually_drop.
    (* StructRecord
      {
        name := "ManuallyDrop";
        const_params := [];
        ty_params := [ "T" ];
        fields := [ ("value", T) ];
      } *)
    
    Module Impl_core_marker_Copy_where_core_marker_Copy_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ 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_Copy_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
    
    Module Impl_core_clone_Clone_where_core_clone_Clone_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ].
      
      (* Clone *)
      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
            Value.StructRecord
              "core::mem::manually_drop::ManuallyDrop"
              [
                ("value",
                  M.call_closure (|
                    M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::mem::manually_drop::ManuallyDrop",
                        "value"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_clone_Clone_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ].
      
      (* Debug *)
      Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        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",
                "debug_struct_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "ManuallyDrop" |);
                M.read (| Value.String "value" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::mem::manually_drop::ManuallyDrop",
                    "value"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
    
    Module Impl_core_default_Default_where_core_default_Default_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ].
      
      (* Default *)
      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
            (Value.StructRecord
              "core::mem::manually_drop::ManuallyDrop"
              [
                ("value",
                  M.call_closure (|
                    M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                    []
                  |))
              ]))
        | _, _, _ => 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_default_Default_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
    
    Module Impl_core_marker_StructuralPartialEq_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ 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_mem_manually_drop_ManuallyDrop_T.
    
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ].
      
      (* PartialEq *)
      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
            M.call_closure (|
              M.get_trait_method (| "core::cmp::PartialEq", T, [ T ], "eq", [] |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::mem::manually_drop::ManuallyDrop",
                  "value"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "core::mem::manually_drop::ManuallyDrop",
                  "value"
                |)
              ]
            |)))
        | _, _, _ => 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_cmp_PartialEq_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
    
    Module Impl_core_cmp_Eq_where_core_cmp_Eq_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ].
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (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 (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::cmp::Eq"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method (assert_receiver_is_total_eq T)) ].
    End Impl_core_cmp_Eq_where_core_cmp_Eq_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
    
    Module Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ].
      
      (* PartialOrd *)
      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
            M.call_closure (|
              M.get_trait_method (| "core::cmp::PartialOrd", T, [ T ], "partial_cmp", [] |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::mem::manually_drop::ManuallyDrop",
                  "value"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "core::mem::manually_drop::ManuallyDrop",
                  "value"
                |)
              ]
            |)))
        | _, _, _ => 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_cmp_PartialOrd_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
    
    Module Impl_core_cmp_Ord_where_core_cmp_Ord_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ].
      
      (* Ord *)
      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
            M.call_closure (|
              M.get_trait_method (| "core::cmp::Ord", T, [], "cmp", [] |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::mem::manually_drop::ManuallyDrop",
                  "value"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "core::mem::manually_drop::ManuallyDrop",
                  "value"
                |)
              ]
            |)))
        | _, _, _ => 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_cmp_Ord_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
    
    Module Impl_core_hash_Hash_where_core_hash_Hash_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ].
      
      (* Hash *)
      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; state ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let state := M.alloc (| state |) in
            M.call_closure (|
              M.get_trait_method (| "core::hash::Hash", T, [], "hash", [ __H ] |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::mem::manually_drop::ManuallyDrop",
                  "value"
                |);
                M.read (| state |)
              ]
            |)))
        | _, _, _ => 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_hash_Hash_T_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
    
    Module Impl_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ].
      
      (*
          pub const fn new(value: T) -> ManuallyDrop<T> {
              ManuallyDrop { value }
          }
      *)
      Definition new (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ value ] =>
          ltac:(M.monadic
            (let value := M.alloc (| value |) in
            Value.StructRecord
              "core::mem::manually_drop::ManuallyDrop"
              [ ("value", M.read (| value |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "new" (new T).
      
      (*
          pub const fn into_inner(slot: ManuallyDrop<T>) -> T {
              slot.value
          }
      *)
      Definition into_inner (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ slot ] =>
          ltac:(M.monadic
            (let slot := M.alloc (| slot |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                slot,
                "core::mem::manually_drop::ManuallyDrop",
                "value"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_into_inner :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "into_inner" (into_inner T).
      
      (*
          pub unsafe fn take(slot: &mut ManuallyDrop<T>) -> T {
              // SAFETY: we are reading from a reference, which is guaranteed
              // to be valid for reads.
              unsafe { ptr::read(&slot.value) }
          }
      *)
      Definition take (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ slot ] =>
          ltac:(M.monadic
            (let slot := M.alloc (| slot |) in
            M.call_closure (|
              M.get_function (| "core::ptr::read", [ T ] |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| slot |),
                  "core::mem::manually_drop::ManuallyDrop",
                  "value"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_take :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "take" (take T).
      (*
          pub unsafe fn drop(slot: &mut ManuallyDrop<T>) {
              // SAFETY: we are dropping the value pointed to by a mutable reference
              // which is guaranteed to be valid for writes.
              // It is up to the caller to make sure that `slot` isn't dropped again.
              unsafe { ptr::drop_in_place(&mut slot.value) }
          }
      *)
      Definition drop (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ slot ] =>
          ltac:(M.monadic
            (let slot := M.alloc (| slot |) in
            M.call_closure (|
              M.get_function (| "core::ptr::drop_in_place", [ T ] |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| slot |),
                  "core::mem::manually_drop::ManuallyDrop",
                  "value"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_drop :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "drop" (drop T).
    End Impl_core_mem_manually_drop_ManuallyDrop_T.
    
    
    Module Impl_core_ops_deref_Deref_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ].
      
      (*     type Target = T; *)
      Definition _Target (T : Ty.t) : Ty.t := T.
      
      (*
          fn deref(&self) -> &T {
              &self.value
          }
      *)
      Definition deref (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.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "core::mem::manually_drop::ManuallyDrop",
              "value"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::ops::deref::Deref"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Target", InstanceField.Ty (_Target T)); ("deref", InstanceField.Method (deref T)) ].
    End Impl_core_ops_deref_Deref_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
    
    Module Impl_core_ops_deref_DerefMut_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ].
      
      (*
          fn deref_mut(&mut self) -> &mut T {
              &mut self.value
          }
      *)
      Definition deref_mut (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.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "core::mem::manually_drop::ManuallyDrop",
              "value"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::ops::deref::DerefMut"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("deref_mut", InstanceField.Method (deref_mut T)) ].
    End Impl_core_ops_deref_DerefMut_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
    
    Module Impl_core_ops_deref_DerefPure_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::ops::deref::DerefPure"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_ops_deref_DerefPure_where_core_marker_Sized_T_for_core_mem_manually_drop_ManuallyDrop_T.
  End manually_drop.
End mem.
