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

Module mem.
  Module maybe_uninit.
    (* Error Union *)
    
    Module Impl_core_marker_Copy_where_core_marker_Copy_T_for_core_mem_maybe_uninit_MaybeUninit_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ 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_for_core_mem_maybe_uninit_MaybeUninit_T.
    
    Module Impl_core_clone_Clone_where_core_marker_Copy_T_for_core_mem_maybe_uninit_MaybeUninit_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ].
      
      (*
          fn clone(&self) -> Self {
              // Not calling `T::clone()`, we cannot know if we are initialized enough for that.
              *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_Copy_T_for_core_mem_maybe_uninit_MaybeUninit_T.
    
    Module Impl_core_fmt_Debug_for_core_mem_maybe_uninit_MaybeUninit_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ].
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              f.pad(type_name::<Self>())
          }
      *)
      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", "pad", [] |),
              [
                M.read (| f |);
                M.call_closure (|
                  M.get_function (|
                    "core::any::type_name",
                    [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                  |),
                  []
                |)
              ]
            |)))
        | _, _, _ => 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_for_core_mem_maybe_uninit_MaybeUninit_T.
    
    Module Impl_core_mem_maybe_uninit_MaybeUninit_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ].
      
      (*
          pub const fn new(val: T) -> MaybeUninit<T> {
              MaybeUninit { value: ManuallyDrop::new(val) }
          }
      *)
      Definition new (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ val ] =>
          ltac:(M.monadic
            (let val := M.alloc (| val |) in
            Value.StructRecord
              "core::mem::maybe_uninit::MaybeUninit"
              [
                ("value",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ],
                      "new",
                      []
                    |),
                    [ M.read (| val |) ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "new" (new T).
      
      (*
          pub const fn uninit() -> MaybeUninit<T> {
              MaybeUninit { uninit: () }
          }
      *)
      Definition uninit (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::maybe_uninit::MaybeUninit"
              [ ("uninit", Value.Tuple []) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_uninit :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "uninit" (uninit T).
      
      (*
          pub const fn uninit_array<const N: usize>() -> [Self; N] {
              [const { MaybeUninit::uninit() }; N]
          }
      *)
      Definition uninit_array
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [ N ], [], [] =>
          ltac:(M.monadic
            (repeat (|
              M.read (|
                M.get_constant (| "core::mem::maybe_uninit::uninit_array_discriminant" |)
              |),
              N
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_uninit_array :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "uninit_array" (uninit_array T).
      
      (*
          pub const fn zeroed() -> MaybeUninit<T> {
              let mut u = MaybeUninit::<T>::uninit();
              // SAFETY: `u.as_mut_ptr()` points to allocated memory.
              unsafe { u.as_mut_ptr().write_bytes(0u8, 1) };
              u
          }
      *)
      Definition zeroed (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 (|
              let~ u :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                      "uninit",
                      []
                    |),
                    []
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "*mut") [] [ T ],
                      "write_bytes",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                          "as_mut_ptr",
                          []
                        |),
                        [ u ]
                      |);
                      Value.Integer IntegerKind.U8 0;
                      Value.Integer IntegerKind.Usize 1
                    ]
                  |)
                |) in
              u
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_zeroed :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "zeroed" (zeroed T).
      
      (*
          pub const fn write(&mut self, val: T) -> &mut T {
              *self = MaybeUninit::new(val);
              // SAFETY: We just initialized this value.
              unsafe { self.assume_init_mut() }
          }
      *)
      Definition write (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; val ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let val := M.alloc (| val |) in
            M.read (|
              let~ _ :=
                M.write (|
                  M.read (| self |),
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                      "new",
                      []
                    |),
                    [ M.read (| val |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                    "assume_init_mut",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_write :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "write" (write T).
      
      (*
          pub const fn as_ptr(&self) -> *const T {
              // `MaybeUninit` and `ManuallyDrop` are both `repr(transparent)` so we can cast the pointer.
              self as *const _ as *const T
          }
      *)
      Definition as_ptr (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.rust_cast (M.read (| M.use (M.alloc (| M.read (| self |) |)) |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_ptr :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_ptr" (as_ptr T).
      
      (*
          pub const fn as_mut_ptr(&mut self) -> *mut T {
              // `MaybeUninit` and `ManuallyDrop` are both `repr(transparent)` so we can cast the pointer.
              self as *mut _ as *mut T
          }
      *)
      Definition as_mut_ptr (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.rust_cast (M.read (| M.use (M.alloc (| M.read (| self |) |)) |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_mut_ptr :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_mut_ptr" (as_mut_ptr T).
      
      (*
          pub const unsafe fn assume_init(self) -> T {
              // SAFETY: the caller must guarantee that `self` is initialized.
              // This also means that `self` must be a `value` variant.
              unsafe {
                  intrinsics::assert_inhabited::<T>();
                  ManuallyDrop::into_inner(self.value)
              }
          }
      *)
      Definition assume_init (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 (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::assert_inhabited", [ T ] |),
                    []
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ T ],
                    "into_inner",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::mem::maybe_uninit::MaybeUninit",
                        "value"
                      |)
                    |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_assume_init :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "assume_init" (assume_init T).
      
      (*
          pub const unsafe fn assume_init_read(&self) -> T {
              // SAFETY: the caller must guarantee that `self` is initialized.
              // Reading from `self.as_ptr()` is safe since `self` should be initialized.
              unsafe {
                  intrinsics::assert_inhabited::<T>();
                  self.as_ptr().read()
              }
          }
      *)
      Definition assume_init_read
          (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 (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::assert_inhabited", [ T ] |),
                    []
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.apply (Ty.path "*const") [] [ T ], "read", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                        "as_ptr",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_assume_init_read :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "assume_init_read" (assume_init_read T).
      
      (*
          pub unsafe fn assume_init_drop(&mut self) {
              // SAFETY: the caller must guarantee that `self` is initialized and
              // satisfies all invariants of `T`.
              // Dropping the value in place is safe if that is the case.
              unsafe { ptr::drop_in_place(self.as_mut_ptr()) }
          }
      *)
      Definition assume_init_drop
          (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.call_closure (|
              M.get_function (| "core::ptr::drop_in_place", [ T ] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                    "as_mut_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_assume_init_drop :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "assume_init_drop" (assume_init_drop T).
      
      (*
          pub const unsafe fn assume_init_ref(&self) -> &T {
              // SAFETY: the caller must guarantee that `self` is initialized.
              // This also means that `self` must be a `value` variant.
              unsafe {
                  intrinsics::assert_inhabited::<T>();
                  &*self.as_ptr()
              }
          }
      *)
      Definition assume_init_ref
          (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 (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::assert_inhabited", [ T ] |),
                    []
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_assume_init_ref :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "assume_init_ref" (assume_init_ref T).
      
      (*
          pub const unsafe fn assume_init_mut(&mut self) -> &mut T {
              // SAFETY: the caller must guarantee that `self` is initialized.
              // This also means that `self` must be a `value` variant.
              unsafe {
                  intrinsics::assert_inhabited::<T>();
                  &mut *self.as_mut_ptr()
              }
          }
      *)
      Definition assume_init_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.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::assert_inhabited", [ T ] |),
                    []
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                    "as_mut_ptr",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_assume_init_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "assume_init_mut" (assume_init_mut T).
      
      (*
          pub const unsafe fn array_assume_init<const N: usize>(array: [Self; N]) -> [T; N] {
              // SAFETY:
              // * The caller guarantees that all elements of the array are initialized
              // * `MaybeUninit<T>` and T are guaranteed to have the same layout
              // * `MaybeUninit` does not drop, so there are no double-frees
              // And thus the conversion is safe
              unsafe {
                  intrinsics::assert_inhabited::<[T; N]>();
                  intrinsics::transmute_unchecked(array)
              }
          }
      *)
      Definition array_assume_init
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [ N ], [], [ array ] =>
          ltac:(M.monadic
            (let array := M.alloc (| array |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::assert_inhabited",
                      [ Ty.apply (Ty.path "array") [ N ] [ T ] ]
                    |),
                    []
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::transmute_unchecked",
                    [
                      Ty.apply
                        (Ty.path "array")
                        [ N ]
                        [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ];
                      Ty.apply (Ty.path "array") [ N ] [ T ]
                    ]
                  |),
                  [ M.read (| array |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_array_assume_init :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "array_assume_init" (array_assume_init T).
      
      (*
          pub const unsafe fn slice_assume_init_ref(slice: &[Self]) -> &[T] {
              // SAFETY: casting `slice` to a `*const [T]` is safe since the caller guarantees that
              // `slice` is initialized, and `MaybeUninit` is guaranteed to have the same layout as `T`.
              // The pointer obtained is valid since it refers to memory owned by `slice` which is a
              // reference and thus guaranteed to be valid for reads.
              unsafe { &*(slice as *const [Self] as *const [T]) }
          }
      *)
      Definition slice_assume_init_ref
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ slice ] =>
          ltac:(M.monadic
            (let slice := M.alloc (| slice |) in
            M.rust_cast (M.read (| M.use (M.alloc (| M.read (| slice |) |)) |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_slice_assume_init_ref :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "slice_assume_init_ref" (slice_assume_init_ref T).
      
      (*
          pub const unsafe fn slice_assume_init_mut(slice: &mut [Self]) -> &mut [T] {
              // SAFETY: similar to safety notes for `slice_get_ref`, but we have a
              // mutable reference which is also guaranteed to be valid for writes.
              unsafe { &mut *(slice as *mut [Self] as *mut [T]) }
          }
      *)
      Definition slice_assume_init_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ slice ] =>
          ltac:(M.monadic
            (let slice := M.alloc (| slice |) in
            M.rust_cast (M.read (| M.use (M.alloc (| M.read (| slice |) |)) |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_slice_assume_init_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "slice_assume_init_mut" (slice_assume_init_mut T).
      
      (*
          pub const fn slice_as_ptr(this: &[MaybeUninit<T>]) -> *const T {
              this.as_ptr() as *const T
          }
      *)
      Definition slice_as_ptr
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ this ] =>
          ltac:(M.monadic
            (let this := M.alloc (| this |) in
            M.rust_cast
              (M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "slice")
                    []
                    [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                  "as_ptr",
                  []
                |),
                [ M.read (| this |) ]
              |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_slice_as_ptr :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "slice_as_ptr" (slice_as_ptr T).
      
      (*
          pub const fn slice_as_mut_ptr(this: &mut [MaybeUninit<T>]) -> *mut T {
              this.as_mut_ptr() as *mut T
          }
      *)
      Definition slice_as_mut_ptr
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ this ] =>
          ltac:(M.monadic
            (let this := M.alloc (| this |) in
            M.rust_cast
              (M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "slice")
                    []
                    [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                  "as_mut_ptr",
                  []
                |),
                [ M.read (| this |) ]
              |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_slice_as_mut_ptr :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "slice_as_mut_ptr" (slice_as_mut_ptr T).
      
      (*
          pub fn copy_from_slice<'a>(this: &'a mut [MaybeUninit<T>], src: &[T]) -> &'a mut [T]
          where
              T: Copy,
          {
              // SAFETY: &[T] and &[MaybeUninit<T>] have the same layout
              let uninit_src: &[MaybeUninit<T>] = unsafe { super::transmute(src) };
      
              this.copy_from_slice(uninit_src);
      
              // SAFETY: Valid elements have just been copied into `this` so it is initialized
              unsafe { MaybeUninit::slice_assume_init_mut(this) }
          }
      *)
      Definition copy_from_slice
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ this; src ] =>
          ltac:(M.monadic
            (let this := M.alloc (| this |) in
            let src := M.alloc (| src |) in
            M.read (|
              let~ uninit_src :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::transmute",
                      [
                        Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ];
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                          ]
                      ]
                    |),
                    [ M.read (| src |) ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                      "copy_from_slice",
                      []
                    |),
                    [ M.read (| this |); M.read (| uninit_src |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                    "slice_assume_init_mut",
                    []
                  |),
                  [ M.read (| this |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_copy_from_slice :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "copy_from_slice" (copy_from_slice T).
      
      (*
          pub fn clone_from_slice<'a>(this: &'a mut [MaybeUninit<T>], src: &[T]) -> &'a mut [T]
          where
              T: Clone,
          {
              // unlike copy_from_slice this does not call clone_from_slice on the slice
              // this is because `MaybeUninit<T: Clone>` does not implement Clone.
      
              assert_eq!(this.len(), src.len(), "destination and source slices have different lengths");
              // NOTE: We need to explicitly slice them to the same length
              // for bounds checking to be elided, and the optimizer will
              // generate memcpy for simple cases (for example T = u8).
              let len = this.len();
              let src = &src[..len];
      
              // guard is needed b/c panic might happen during a clone
              let mut guard = Guard { slice: this, initialized: 0 };
      
              for i in 0..len {
                  guard.slice[i].write(src[i].clone());
                  guard.initialized += 1;
              }
      
              super::forget(guard);
      
              // SAFETY: Valid elements have just been written into `this` so it is initialized
              unsafe { MaybeUninit::slice_assume_init_mut(this) }
          }
      *)
      Definition clone_from_slice
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ this; src ] =>
          ltac:(M.monadic
            (let this := M.alloc (| this |) in
            let src := M.alloc (| src |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (|
                    Value.Tuple
                      [
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "slice")
                                []
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ],
                              "len",
                              []
                            |),
                            [ M.read (| this |) ]
                          |)
                        |);
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ T ],
                              "len",
                              []
                            |),
                            [ M.read (| src |) ]
                          |)
                        |)
                      ]
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let left_val := M.copy (| γ0_0 |) in
                        let right_val := M.copy (| γ0_1 |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        BinOp.eq (|
                                          M.read (| M.read (| left_val |) |),
                                          M.read (| M.read (| right_val |) |)
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ kind :=
                                        M.alloc (|
                                          Value.StructTuple "core::panicking::AssertKind::Eq" []
                                        |) in
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_function (|
                                            "core::panicking::assert_failed",
                                            [ Ty.path "usize"; Ty.path "usize" ]
                                          |),
                                          [
                                            M.read (| kind |);
                                            M.read (| left_val |);
                                            M.read (| right_val |);
                                            Value.StructTuple
                                              "core::option::Option::Some"
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "core::fmt::Arguments",
                                                    "new_const",
                                                    []
                                                  |),
                                                  [
                                                    M.alloc (|
                                                      Value.Array
                                                        [
                                                          M.read (|
                                                            Value.String
                                                              "destination and source slices have different lengths"
                                                          |)
                                                        ]
                                                    |)
                                                  ]
                                                |)
                                              ]
                                          ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |)))
                  ]
                |) in
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                      "len",
                      []
                    |),
                    [ M.read (| this |) ]
                  |)
                |) in
              let~ src :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::index::Index",
                      Ty.apply (Ty.path "slice") [] [ T ],
                      [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ],
                      "index",
                      []
                    |),
                    [
                      M.read (| src |);
                      Value.StructRecord "core::ops::range::RangeTo" [ ("end_", M.read (| len |)) ]
                    ]
                  |)
                |) in
              let~ guard :=
                M.alloc (|
                  Value.StructRecord
                    "core::mem::maybe_uninit::Guard"
                    [
                      ("slice", M.read (| this |));
                      ("initialized", Value.Integer IntegerKind.Usize 0)
                    ]
                |) in
              let~ _ :=
                M.use
                  (M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::collect::IntoIterator",
                          Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          Value.StructRecord
                            "core::ops::range::Range"
                            [
                              ("start", Value.Integer IntegerKind.Usize 0);
                              ("end_", M.read (| len |))
                            ]
                        ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let iter := M.copy (| γ |) in
                          M.loop (|
                            ltac:(M.monadic
                              (let~ _ :=
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::ops::range::Range")
                                          []
                                          [ Ty.path "usize" ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ iter ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::option::Option::Some",
                                            0
                                          |) in
                                        let i := M.copy (| γ0_0 |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                                  []
                                                  [ T ],
                                                "write",
                                                []
                                              |),
                                              [
                                                M.SubPointer.get_array_field (|
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      guard,
                                                      "core::mem::maybe_uninit::Guard",
                                                      "slice"
                                                    |)
                                                  |),
                                                  i
                                                |);
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::clone::Clone",
                                                    T,
                                                    [],
                                                    "clone",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| src |),
                                                      i
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          let β :=
                                            M.SubPointer.get_struct_record_field (|
                                              guard,
                                              "core::mem::maybe_uninit::Guard",
                                              "initialized"
                                            |) in
                                          M.write (|
                                            β,
                                            BinOp.Wrap.add (|
                                              M.read (| β |),
                                              Value.Integer IntegerKind.Usize 1
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::mem::forget",
                      [ Ty.apply (Ty.path "core::mem::maybe_uninit::Guard") [] [ T ] ]
                    |),
                    [ M.read (| guard |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                    "slice_assume_init_mut",
                    []
                  |),
                  [ M.read (| this |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_clone_from_slice :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "clone_from_slice" (clone_from_slice T).
      
      (*
          pub fn fill<'a>(this: &'a mut [MaybeUninit<T>], value: T) -> &'a mut [T]
          where
              T: Clone,
          {
              SpecFill::spec_fill(this, value);
              // SAFETY: Valid elements have just been filled into `this` so it is initialized
              unsafe { MaybeUninit::slice_assume_init_mut(this) }
          }
      *)
      Definition fill (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ this; value ] =>
          ltac:(M.monadic
            (let this := M.alloc (| this |) in
            let value := M.alloc (| value |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::mem::maybe_uninit::SpecFill",
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                      [ T ],
                      "spec_fill",
                      []
                    |),
                    [ M.read (| this |); M.read (| value |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                    "slice_assume_init_mut",
                    []
                  |),
                  [ M.read (| this |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_fill :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "fill" (fill T).
      
      (*
          pub fn fill_with<'a, F>(this: &'a mut [MaybeUninit<T>], mut f: F) -> &'a mut [T]
          where
              F: FnMut() -> T,
          {
              let mut guard = Guard { slice: this, initialized: 0 };
      
              for element in guard.slice.iter_mut() {
                  element.write(f());
                  guard.initialized += 1;
              }
      
              super::forget(guard);
      
              // SAFETY: Valid elements have just been written into `this` so it is initialized
              unsafe { MaybeUninit::slice_assume_init_mut(this) }
          }
      *)
      Definition fill_with (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ F ], [ this; f ] =>
          ltac:(M.monadic
            (let this := M.alloc (| this |) in
            let f := M.alloc (| f |) in
            M.read (|
              let~ guard :=
                M.alloc (|
                  Value.StructRecord
                    "core::mem::maybe_uninit::Guard"
                    [
                      ("slice", M.read (| this |));
                      ("initialized", Value.Integer IntegerKind.Usize 0)
                    ]
                |) in
              let~ _ :=
                M.use
                  (M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::collect::IntoIterator",
                          Ty.apply
                            (Ty.path "core::slice::iter::IterMut")
                            []
                            [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "slice")
                                []
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ],
                              "iter_mut",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  guard,
                                  "core::mem::maybe_uninit::Guard",
                                  "slice"
                                |)
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let iter := M.copy (| γ |) in
                          M.loop (|
                            ltac:(M.monadic
                              (let~ _ :=
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::slice::iter::IterMut")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                              []
                                              [ T ]
                                          ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ iter ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::option::Option::Some",
                                            0
                                          |) in
                                        let element := M.copy (| γ0_0 |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                                  []
                                                  [ T ],
                                                "write",
                                                []
                                              |),
                                              [
                                                M.read (| element |);
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::function::FnMut",
                                                    F,
                                                    [ Ty.tuple [] ],
                                                    "call_mut",
                                                    []
                                                  |),
                                                  [ f; Value.Tuple [] ]
                                                |)
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          let β :=
                                            M.SubPointer.get_struct_record_field (|
                                              guard,
                                              "core::mem::maybe_uninit::Guard",
                                              "initialized"
                                            |) in
                                          M.write (|
                                            β,
                                            BinOp.Wrap.add (|
                                              M.read (| β |),
                                              Value.Integer IntegerKind.Usize 1
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::mem::forget",
                      [ Ty.apply (Ty.path "core::mem::maybe_uninit::Guard") [] [ T ] ]
                    |),
                    [ M.read (| guard |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                    "slice_assume_init_mut",
                    []
                  |),
                  [ M.read (| this |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_fill_with :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "fill_with" (fill_with T).
      
      (*
          pub fn fill_from<'a, I>(
              this: &'a mut [MaybeUninit<T>],
              it: I,
          ) -> (&'a mut [T], &'a mut [MaybeUninit<T>])
          where
              I: IntoIterator<Item = T>,
          {
              let iter = it.into_iter();
              let mut guard = Guard { slice: this, initialized: 0 };
      
              for (element, val) in guard.slice.iter_mut().zip(iter) {
                  element.write(val);
                  guard.initialized += 1;
              }
      
              let initialized_len = guard.initialized;
              super::forget(guard);
      
              // SAFETY: guard.initialized <= this.len()
              let (initted, remainder) = unsafe { this.split_at_mut_unchecked(initialized_len) };
      
              // SAFETY: Valid elements have just been written into `init`, so that portion
              // of `this` is initialized.
              (unsafe { MaybeUninit::slice_assume_init_mut(initted) }, remainder)
          }
      *)
      Definition fill_from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ _ as I ], [ this; it ] =>
          ltac:(M.monadic
            (let this := M.alloc (| this |) in
            let it := M.alloc (| it |) in
            M.read (|
              let~ iter :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::collect::IntoIterator",
                      I,
                      [],
                      "into_iter",
                      []
                    |),
                    [ M.read (| it |) ]
                  |)
                |) in
              let~ guard :=
                M.alloc (|
                  Value.StructRecord
                    "core::mem::maybe_uninit::Guard"
                    [
                      ("slice", M.read (| this |));
                      ("initialized", Value.Integer IntegerKind.Usize 0)
                    ]
                |) in
              let~ _ :=
                M.use
                  (M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::collect::IntoIterator",
                          Ty.apply
                            (Ty.path "core::iter::adapters::zip::Zip")
                            []
                            [
                              Ty.apply
                                (Ty.path "core::slice::iter::IterMut")
                                []
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ];
                              Ty.associated
                            ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply
                                (Ty.path "core::slice::iter::IterMut")
                                []
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                                ],
                              [],
                              "zip",
                              [ Ty.associated ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "slice")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                        []
                                        [ T ]
                                    ],
                                  "iter_mut",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      guard,
                                      "core::mem::maybe_uninit::Guard",
                                      "slice"
                                    |)
                                  |)
                                ]
                              |);
                              M.read (| iter |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let iter := M.copy (| γ |) in
                          M.loop (|
                            ltac:(M.monadic
                              (let~ _ :=
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::iter::adapters::zip::Zip")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::slice::iter::IterMut")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                                  []
                                                  [ T ]
                                              ];
                                            Ty.associated
                                          ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ iter ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::option::Option::Some",
                                            0
                                          |) in
                                        let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                        let element := M.copy (| γ1_0 |) in
                                        let val := M.copy (| γ1_1 |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                                  []
                                                  [ T ],
                                                "write",
                                                []
                                              |),
                                              [ M.read (| element |); M.read (| val |) ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          let β :=
                                            M.SubPointer.get_struct_record_field (|
                                              guard,
                                              "core::mem::maybe_uninit::Guard",
                                              "initialized"
                                            |) in
                                          M.write (|
                                            β,
                                            BinOp.Wrap.add (|
                                              M.read (| β |),
                                              Value.Integer IntegerKind.Usize 1
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) in
              let~ initialized_len :=
                M.copy (|
                  M.SubPointer.get_struct_record_field (|
                    guard,
                    "core::mem::maybe_uninit::Guard",
                    "initialized"
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::mem::forget",
                      [ Ty.apply (Ty.path "core::mem::maybe_uninit::Guard") [] [ T ] ]
                    |),
                    [ M.read (| guard |) ]
                  |)
                |) in
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                      "split_at_mut_unchecked",
                      []
                    |),
                    [ M.read (| this |); M.read (| initialized_len |) ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let initted := M.copy (| γ0_0 |) in
                      let remainder := M.copy (| γ0_1 |) in
                      M.alloc (|
                        Value.Tuple
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                                "slice_assume_init_mut",
                                []
                              |),
                              [ M.read (| initted |) ]
                            |);
                            M.read (| remainder |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_fill_from :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "fill_from" (fill_from T).
      
      (*
          pub fn as_bytes(&self) -> &[MaybeUninit<u8>] {
              // SAFETY: MaybeUninit<u8> is always valid, even for padding bytes
              unsafe {
                  slice::from_raw_parts(self.as_ptr() as *const MaybeUninit<u8>, mem::size_of::<T>())
              }
          }
      *)
      Definition as_bytes (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.call_closure (|
              M.get_function (|
                "core::slice::raw::from_raw_parts",
                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ]
              |),
              [
                M.rust_cast
                  (M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [ M.read (| self |) ]
                  |));
                M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_bytes :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_bytes" (as_bytes T).
      
      (*
          pub fn as_bytes_mut(&mut self) -> &mut [MaybeUninit<u8>] {
              // SAFETY: MaybeUninit<u8> is always valid, even for padding bytes
              unsafe {
                  slice::from_raw_parts_mut(
                      self.as_mut_ptr() as *mut MaybeUninit<u8>,
                      mem::size_of::<T>(),
                  )
              }
          }
      *)
      Definition as_bytes_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.call_closure (|
              M.get_function (|
                "core::slice::raw::from_raw_parts_mut",
                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ]
              |),
              [
                M.rust_cast
                  (M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                      "as_mut_ptr",
                      []
                    |),
                    [ M.read (| self |) ]
                  |));
                M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_bytes_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "as_bytes_mut" (as_bytes_mut T).
      
      (*
          pub fn slice_as_bytes(this: &[MaybeUninit<T>]) -> &[MaybeUninit<u8>] {
              let bytes = mem::size_of_val(this);
              // SAFETY: MaybeUninit<u8> is always valid, even for padding bytes
              unsafe { slice::from_raw_parts(this.as_ptr() as *const MaybeUninit<u8>, bytes) }
          }
      *)
      Definition slice_as_bytes
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ this ] =>
          ltac:(M.monadic
            (let this := M.alloc (| this |) in
            M.read (|
              let~ bytes :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::mem::size_of_val",
                      [
                        Ty.apply
                          (Ty.path "slice")
                          []
                          [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                      ]
                    |),
                    [ M.read (| this |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::slice::raw::from_raw_parts",
                    [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ]
                    ]
                  |),
                  [
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                          "as_ptr",
                          []
                        |),
                        [ M.read (| this |) ]
                      |));
                    M.read (| bytes |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_slice_as_bytes :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "slice_as_bytes" (slice_as_bytes T).
      
      (*
          pub fn slice_as_bytes_mut(this: &mut [MaybeUninit<T>]) -> &mut [MaybeUninit<u8>] {
              let bytes = mem::size_of_val(this);
              // SAFETY: MaybeUninit<u8> is always valid, even for padding bytes
              unsafe { slice::from_raw_parts_mut(this.as_mut_ptr() as *mut MaybeUninit<u8>, bytes) }
          }
      *)
      Definition slice_as_bytes_mut
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ this ] =>
          ltac:(M.monadic
            (let this := M.alloc (| this |) in
            M.read (|
              let~ bytes :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::mem::size_of_val",
                      [
                        Ty.apply
                          (Ty.path "slice")
                          []
                          [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                      ]
                    |),
                    [ M.read (| this |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::slice::raw::from_raw_parts_mut",
                    [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ]
                    ]
                  |),
                  [
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                          "as_mut_ptr",
                          []
                        |),
                        [ M.read (| this |) ]
                      |));
                    M.read (| bytes |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_slice_as_bytes_mut :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "slice_as_bytes_mut" (slice_as_bytes_mut T).
    End Impl_core_mem_maybe_uninit_MaybeUninit_T.
    
    Module Impl_core_mem_maybe_uninit_MaybeUninit_array_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply
          (Ty.path "core::mem::maybe_uninit::MaybeUninit")
          []
          [ Ty.apply (Ty.path "array") [ N ] [ T ] ].
      
      (*
          pub const fn transpose(self) -> [MaybeUninit<T>; N] {
              // SAFETY: T and MaybeUninit<T> have the same layout
              unsafe { intrinsics::transmute_unchecked(self) }
          }
      *)
      Definition transpose
          (N : Value.t)
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (|
                "core::intrinsics::transmute_unchecked",
                [
                  Ty.apply
                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                    []
                    [ Ty.apply (Ty.path "array") [ N ] [ T ] ];
                  Ty.apply
                    (Ty.path "array")
                    [ N ]
                    [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                ]
              |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_transpose :
        forall (N : Value.t) (T : Ty.t),
        M.IsAssociatedFunction (Self N T) "transpose" (transpose N T).
    End Impl_core_mem_maybe_uninit_MaybeUninit_array_N_T.
    
    Module Impl_array_N_core_mem_maybe_uninit_MaybeUninit_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply
          (Ty.path "array")
          [ N ]
          [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ].
      
      (*
          pub const fn transpose(self) -> MaybeUninit<[T; N]> {
              // SAFETY: T and MaybeUninit<T> have the same layout
              unsafe { intrinsics::transmute_unchecked(self) }
          }
      *)
      Definition transpose
          (N : Value.t)
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (|
                "core::intrinsics::transmute_unchecked",
                [
                  Ty.apply
                    (Ty.path "array")
                    [ N ]
                    [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ];
                  Ty.apply
                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                    []
                    [ Ty.apply (Ty.path "array") [ N ] [ T ] ]
                ]
              |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_transpose :
        forall (N : Value.t) (T : Ty.t),
        M.IsAssociatedFunction (Self N T) "transpose" (transpose N T).
    End Impl_array_N_core_mem_maybe_uninit_MaybeUninit_T.
    
    (* StructRecord
      {
        name := "Guard";
        const_params := [];
        ty_params := [ "T" ];
        fields :=
          [
            ("slice",
              Ty.apply
                (Ty.path "&mut")
                []
                [
                  Ty.apply
                    (Ty.path "slice")
                    []
                    [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
                ]);
            ("initialized", Ty.path "usize")
          ];
      } *)
    
    Module Impl_core_ops_drop_Drop_for_core_mem_maybe_uninit_Guard_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::mem::maybe_uninit::Guard") [] [ T ].
      
      (*
          fn drop(&mut self) {
              let initialized_part = &mut self.slice[..self.initialized];
              // SAFETY: this raw sub-slice will contain only initialized objects.
              unsafe {
                  crate::ptr::drop_in_place(MaybeUninit::slice_assume_init_mut(initialized_part));
              }
          }
      *)
      Definition drop (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 (|
              let~ initialized_part :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::index::IndexMut",
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                      [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ],
                      "index_mut",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::mem::maybe_uninit::Guard",
                          "slice"
                        |)
                      |);
                      Value.StructRecord
                        "core::ops::range::RangeTo"
                        [
                          ("end_",
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::mem::maybe_uninit::Guard",
                                "initialized"
                              |)
                            |))
                        ]
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::ptr::drop_in_place",
                      [ Ty.apply (Ty.path "slice") [] [ T ] ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                          "slice_assume_init_mut",
                          []
                        |),
                        [ M.read (| initialized_part |) ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::ops::drop::Drop"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("drop", InstanceField.Method (drop T)) ].
    End Impl_core_ops_drop_Drop_for_core_mem_maybe_uninit_Guard_T.
    
    (* Trait *)
    (* Empty module 'SpecFill' *)
    
    Module Impl_core_mem_maybe_uninit_SpecFill_where_core_clone_Clone_T_T_for_slice_core_mem_maybe_uninit_MaybeUninit_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply
          (Ty.path "slice")
          []
          [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ].
      
      (*
          default fn spec_fill(&mut self, value: T) {
              let mut guard = Guard { slice: self, initialized: 0 };
      
              if let Some((last, elems)) = guard.slice.split_last_mut() {
                  for el in elems {
                      el.write(value.clone());
                      guard.initialized += 1;
                  }
      
                  last.write(value);
              }
              super::forget(guard);
          }
      *)
      Definition spec_fill (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let value := M.alloc (| value |) in
            M.read (|
              let~ guard :=
                M.alloc (|
                  Value.StructRecord
                    "core::mem::maybe_uninit::Guard"
                    [
                      ("slice", M.read (| self |));
                      ("initialized", Value.Integer IntegerKind.Usize 0)
                    ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                      []
                                      [ T ]
                                  ],
                                "split_last_mut",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    guard,
                                    "core::mem::maybe_uninit::Guard",
                                    "slice"
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                        let last := M.copy (| γ1_0 |) in
                        let elems := M.copy (| γ1_1 |) in
                        let~ _ :=
                          M.use
                            (M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::collect::IntoIterator",
                                    Ty.apply
                                      (Ty.path "&mut")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "slice")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                              []
                                              [ T ]
                                          ]
                                      ],
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [ M.read (| elems |) ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.loop (|
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::iter::traits::iterator::Iterator",
                                                  Ty.apply
                                                    (Ty.path "core::slice::iter::IterMut")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path
                                                          "core::mem::maybe_uninit::MaybeUninit")
                                                        []
                                                        [ T ]
                                                    ],
                                                  [],
                                                  "next",
                                                  []
                                                |),
                                                [ iter ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let _ :=
                                                    M.is_struct_tuple (|
                                                      γ,
                                                      "core::option::Option::None"
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (| M.read (| M.break (||) |) |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let el := M.copy (| γ0_0 |) in
                                                  let~ _ :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path
                                                              "core::mem::maybe_uninit::MaybeUninit")
                                                            []
                                                            [ T ],
                                                          "write",
                                                          []
                                                        |),
                                                        [
                                                          M.read (| el |);
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::clone::Clone",
                                                              T,
                                                              [],
                                                              "clone",
                                                              []
                                                            |),
                                                            [ value ]
                                                          |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    let β :=
                                                      M.SubPointer.get_struct_record_field (|
                                                        guard,
                                                        "core::mem::maybe_uninit::Guard",
                                                        "initialized"
                                                      |) in
                                                    M.write (|
                                                      β,
                                                      BinOp.Wrap.add (|
                                                        M.read (| β |),
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                    |)))
                              ]
                            |)) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                                "write",
                                []
                              |),
                              [ M.read (| last |); M.read (| value |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::mem::forget",
                      [ Ty.apply (Ty.path "core::mem::maybe_uninit::Guard") [] [ T ] ]
                    |),
                    [ M.read (| guard |) ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::mem::maybe_uninit::SpecFill"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) T ]
          (* Instance *) [ ("spec_fill", InstanceField.Method (spec_fill T)) ].
    End Impl_core_mem_maybe_uninit_SpecFill_where_core_clone_Clone_T_T_for_slice_core_mem_maybe_uninit_MaybeUninit_T.
    
    Module Impl_core_mem_maybe_uninit_SpecFill_where_core_marker_Copy_T_T_for_slice_core_mem_maybe_uninit_MaybeUninit_T.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply
          (Ty.path "slice")
          []
          [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ].
      
      (*
          fn spec_fill(&mut self, value: T) {
              self.fill(MaybeUninit::new(value));
          }
      *)
      Definition spec_fill (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let value := M.alloc (| value |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                      "fill",
                      []
                    |),
                    [
                      M.read (| self |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                          "new",
                          []
                        |),
                        [ M.read (| value |) ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::mem::maybe_uninit::SpecFill"
          (Self T)
          (* Trait polymorphic types *) [ (* T *) T ]
          (* Instance *) [ ("spec_fill", InstanceField.Method (spec_fill T)) ].
    End Impl_core_mem_maybe_uninit_SpecFill_where_core_marker_Copy_T_T_for_slice_core_mem_maybe_uninit_MaybeUninit_T.
  End maybe_uninit.
End mem.
