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

Module clone.
  (* Trait *)
  Module Clone.
    Definition clone_from (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; source ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let source := M.alloc (| source |) in
          M.read (|
            M.write (|
              M.read (| self |),
              M.call_closure (|
                M.get_trait_method (| "core::clone::Clone", Self, [], "clone", [] |),
                [ M.read (| source |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_clone_from :
      M.IsProvidedMethod "core::clone::Clone" "clone_from" clone_from.
  End Clone.
  
  (* StructRecord
    {
      name := "AssertParamIsClone";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ ("_field", Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ]) ];
    } *)
  
  (* StructRecord
    {
      name := "AssertParamIsCopy";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ ("_field", Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ]) ];
    } *)
  
  (* Trait *)
  (* Empty module 'CloneToUninit' *)
  
  Module Impl_core_clone_CloneToUninit_where_core_clone_Clone_T_for_T.
    Definition Self (T : Ty.t) : Ty.t := T.
    
    (*
        unsafe fn clone_to_uninit(&self, dst: *mut Self) {
            // SAFETY: we're calling a specialization with the same contract
            unsafe { <T as self::uninit::CopySpec>::clone_one(self, dst) }
        }
    *)
    Definition clone_to_uninit
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; dst ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let dst := M.alloc (| dst |) in
          M.call_closure (|
            M.get_trait_method (| "core::clone::uninit::CopySpec", T, [], "clone_one", [] |),
            [ M.read (| self |); M.read (| dst |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::clone::CloneToUninit"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone_to_uninit", InstanceField.Method (clone_to_uninit T)) ].
  End Impl_core_clone_CloneToUninit_where_core_clone_Clone_T_for_T.
  
  Module Impl_core_clone_CloneToUninit_where_core_clone_Clone_T_for_slice_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
    
    (*
        unsafe fn clone_to_uninit(&self, dst: *mut Self) {
            // SAFETY: we're calling a specialization with the same contract
            unsafe { <T as self::uninit::CopySpec>::clone_slice(self, dst) }
        }
    *)
    Definition clone_to_uninit
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; dst ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let dst := M.alloc (| dst |) in
          M.call_closure (|
            M.get_trait_method (| "core::clone::uninit::CopySpec", T, [], "clone_slice", [] |),
            [ M.read (| self |); M.read (| dst |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::clone::CloneToUninit"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone_to_uninit", InstanceField.Method (clone_to_uninit T)) ].
  End Impl_core_clone_CloneToUninit_where_core_clone_Clone_T_for_slice_T.
  
  Module Impl_core_clone_CloneToUninit_for_str.
    Definition Self : Ty.t := Ty.path "str".
    
    (*
        unsafe fn clone_to_uninit(&self, dst: *mut Self) {
            // SAFETY: str is just a [u8] with UTF-8 invariant
            unsafe { self.as_bytes().clone_to_uninit(dst as *mut [u8]) }
        }
    *)
    Definition clone_to_uninit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; dst ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let dst := M.alloc (| dst |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::clone::CloneToUninit",
              Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
              [],
              "clone_to_uninit",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                [ M.read (| self |) ]
              |);
              M.rust_cast (M.read (| dst |))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::CloneToUninit"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone_to_uninit", InstanceField.Method clone_to_uninit) ].
  End Impl_core_clone_CloneToUninit_for_str.
  
  Module Impl_core_clone_CloneToUninit_for_core_ffi_c_str_CStr.
    Definition Self : Ty.t := Ty.path "core::ffi::c_str::CStr".
    
    (*
        unsafe fn clone_to_uninit(&self, dst: *mut Self) {
            // SAFETY: For now, CStr is just a #[repr(trasnsparent)] [c_char] with some invariants.
            // And we can cast [c_char] to [u8] on all supported platforms (see: to_bytes_with_nul).
            // The pointer metadata properly preserves the length (NUL included).
            // See: `cstr_metadata_is_length_with_nul` in tests.
            unsafe { self.to_bytes_with_nul().clone_to_uninit(dst as *mut [u8]) }
        }
    *)
    Definition clone_to_uninit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; dst ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let dst := M.alloc (| dst |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::clone::CloneToUninit",
              Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
              [],
              "clone_to_uninit",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::ffi::c_str::CStr",
                  "to_bytes_with_nul",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.rust_cast (M.read (| dst |))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::CloneToUninit"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone_to_uninit", InstanceField.Method clone_to_uninit) ].
  End Impl_core_clone_CloneToUninit_for_core_ffi_c_str_CStr.
  
  Module impls.
    Module Impl_core_clone_Clone_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_usize.
    
    Module Impl_core_clone_Clone_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_u8.
    
    Module Impl_core_clone_Clone_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_u16.
    
    Module Impl_core_clone_Clone_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_u32.
    
    Module Impl_core_clone_Clone_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_u64.
    
    Module Impl_core_clone_Clone_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_u128.
    
    Module Impl_core_clone_Clone_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_isize.
    
    Module Impl_core_clone_Clone_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_i8.
    
    Module Impl_core_clone_Clone_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_i16.
    
    Module Impl_core_clone_Clone_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_i32.
    
    Module Impl_core_clone_Clone_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_i64.
    
    Module Impl_core_clone_Clone_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_i128.
    
    Module Impl_core_clone_Clone_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_f16.
    
    Module Impl_core_clone_Clone_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_f32.
    
    Module Impl_core_clone_Clone_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_f64.
    
    Module Impl_core_clone_Clone_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_f128.
    
    Module Impl_core_clone_Clone_for_bool.
      Definition Self : Ty.t := Ty.path "bool".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_bool.
    
    Module Impl_core_clone_Clone_for_char.
      Definition Self : Ty.t := Ty.path "char".
      
      (*
                          fn clone(&self) -> Self {
                              *self
                          }
      *)
      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_char.
    
    Module Impl_core_clone_Clone_for_never.
      Definition Self : Ty.t := Ty.path "never".
      
      (*
              fn clone(&self) -> Self {
                  *self
              }
      *)
      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_never.
    
    Module Impl_core_clone_Clone_where_core_marker_Sized_T_for_pointer_const_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ 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 (| M.read (| self |) |)))
        | _, _, _ => 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_pointer_const_T.
    
    Module Impl_core_clone_Clone_where_core_marker_Sized_T_for_pointer_mut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*mut") [] [ 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 (| M.read (| self |) |)))
        | _, _, _ => 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_pointer_mut_T.
    
    Module Impl_core_clone_Clone_where_core_marker_Sized_T_for_ref__T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ 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 (| M.read (| self |) |)))
        | _, _, _ => 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_ref__T.
    
    Module Impl_core_clone_Clone_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::clone::Clone"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_clone_Clone_where_core_marker_Sized_T_for_ref_mut_T.
  End impls.
End clone.
