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

Module array.
  Module iter.
    (* StructRecord
      {
        name := "IntoIter";
        const_params := [ "N" ];
        ty_params := [ "T" ];
        fields :=
          [
            ("data",
              Ty.apply
                (Ty.path "array")
                [ N ]
                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]);
            ("alive", Ty.path "core::ops::index_range::IndexRange")
          ];
      } *)
    
    Module Impl_core_iter_traits_collect_IntoIterator_for_array_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
      
      (*     type Item = T; *)
      Definition _Item (N : Value.t) (T : Ty.t) : Ty.t := T.
      
      (*     type IntoIter = IntoIter<T, N>; *)
      Definition _IntoIter (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ].
      
      (*
          fn into_iter(self) -> Self::IntoIter {
              // SAFETY: The transmute here is actually safe. The docs of `MaybeUninit`
              // promise:
              //
              // > `MaybeUninit<T>` is guaranteed to have the same size and alignment
              // > as `T`.
              //
              // The docs even show a transmute from an array of `MaybeUninit<T>` to
              // an array of `T`.
              //
              // With that, this initialization satisfies the invariants.
              //
              // FIXME: If normal `transmute` ever gets smart enough to allow this
              // directly, use it instead of `transmute_unchecked`.
              let data: [MaybeUninit<T>; N] = unsafe { transmute_unchecked(self) };
              IntoIter { data, alive: IndexRange::zero_to(N) }
          }
      *)
      Definition into_iter
          (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.read (|
              let~ data :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::transmute_unchecked",
                      [
                        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 |) ]
                  |)
                |) in
              M.alloc (|
                Value.StructRecord
                  "core::array::iter::IntoIter"
                  [
                    ("data", M.read (| data |));
                    ("alive",
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::ops::index_range::IndexRange",
                          "zero_to",
                          []
                        |),
                        [ M.read (| M.get_constant (| "core::array::iter::N" |) |) ]
                      |))
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::collect::IntoIterator"
          (Self N T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item N T));
            ("IntoIter", InstanceField.Ty (_IntoIter N T));
            ("into_iter", InstanceField.Method (into_iter N T))
          ].
    End Impl_core_iter_traits_collect_IntoIterator_for_array_N_T.
    
    Module Impl_core_array_iter_IntoIter_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ].
      
      (*
          pub fn new(array: [T; N]) -> Self {
              IntoIterator::into_iter(array)
          }
      *)
      Definition new
          (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
        | [], [], [ array ] =>
          ltac:(M.monadic
            (let array := M.alloc (| array |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::collect::IntoIterator",
                Ty.apply (Ty.path "array") [ N ] [ T ],
                [],
                "into_iter",
                []
              |),
              [ M.read (| array |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new :
        forall (N : Value.t) (T : Ty.t),
        M.IsAssociatedFunction (Self N T) "new" (new N T).
      
      (*
          pub const unsafe fn new_unchecked(
              buffer: [MaybeUninit<T>; N],
              initialized: Range<usize>,
          ) -> Self {
              // SAFETY: one of our safety conditions is that the range is canonical.
              let alive = unsafe { IndexRange::new_unchecked(initialized.start, initialized.end) };
              Self { data: buffer, alive }
          }
      *)
      Definition new_unchecked
          (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
        | [], [], [ buffer; initialized ] =>
          ltac:(M.monadic
            (let buffer := M.alloc (| buffer |) in
            let initialized := M.alloc (| initialized |) in
            M.read (|
              let~ alive :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::ops::index_range::IndexRange",
                      "new_unchecked",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          initialized,
                          "core::ops::range::Range",
                          "start"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          initialized,
                          "core::ops::range::Range",
                          "end"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                Value.StructRecord
                  "core::array::iter::IntoIter"
                  [ ("data", M.read (| buffer |)); ("alive", M.read (| alive |)) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_unchecked :
        forall (N : Value.t) (T : Ty.t),
        M.IsAssociatedFunction (Self N T) "new_unchecked" (new_unchecked N T).
      
      (*
          pub const fn empty() -> Self {
              let buffer = [const { MaybeUninit::uninit() }; N];
              let initialized = 0..0;
      
              // SAFETY: We're telling it that none of the elements are initialized,
              // which is trivially true. And ∀N: usize, 0 <= N.
              unsafe { Self::new_unchecked(buffer, initialized) }
          }
      *)
      Definition empty
          (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
        | [], [], [] =>
          ltac:(M.monadic
            (M.read (|
              let~ buffer :=
                M.alloc (|
                  repeat (|
                    M.read (| M.get_constant (| "core::array::iter::empty_discriminant" |) |),
                    N
                  |)
                |) in
              let~ initialized :=
                M.alloc (|
                  Value.StructRecord
                    "core::ops::range::Range"
                    [
                      ("start", Value.Integer IntegerKind.Usize 0);
                      ("end_", Value.Integer IntegerKind.Usize 0)
                    ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ],
                    "new_unchecked",
                    []
                  |),
                  [ M.read (| buffer |); M.read (| initialized |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_empty :
        forall (N : Value.t) (T : Ty.t),
        M.IsAssociatedFunction (Self N T) "empty" (empty N T).
      
      (*
          pub fn as_slice(&self) -> &[T] {
              // SAFETY: We know that all elements within `alive` are properly initialized.
              unsafe {
                  let slice = self.data.get_unchecked(self.alive.clone());
                  MaybeUninit::slice_assume_init_ref(slice)
              }
          }
      *)
      Definition as_slice
          (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.read (|
              let~ slice :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                      "get_unchecked",
                      [ Ty.path "core::ops::index_range::IndexRange" ]
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::array::iter::IntoIter",
                        "data"
                      |);
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::clone::Clone",
                          Ty.path "core::ops::index_range::IndexRange",
                          [],
                          "clone",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::array::iter::IntoIter",
                            "alive"
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                    "slice_assume_init_ref",
                    []
                  |),
                  [ M.read (| slice |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_slice :
        forall (N : Value.t) (T : Ty.t),
        M.IsAssociatedFunction (Self N T) "as_slice" (as_slice N T).
      
      (*
          pub fn as_mut_slice(&mut self) -> &mut [T] {
              // SAFETY: We know that all elements within `alive` are properly initialized.
              unsafe {
                  let slice = self.data.get_unchecked_mut(self.alive.clone());
                  MaybeUninit::slice_assume_init_mut(slice)
              }
          }
      *)
      Definition as_mut_slice
          (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.read (|
              let~ slice :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                      "get_unchecked_mut",
                      [ Ty.path "core::ops::index_range::IndexRange" ]
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::array::iter::IntoIter",
                        "data"
                      |);
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::clone::Clone",
                          Ty.path "core::ops::index_range::IndexRange",
                          [],
                          "clone",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::array::iter::IntoIter",
                            "alive"
                          |)
                        ]
                      |)
                    ]
                  |)
                |) 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 (| slice |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_mut_slice :
        forall (N : Value.t) (T : Ty.t),
        M.IsAssociatedFunction (Self N T) "as_mut_slice" (as_mut_slice N T).
    End Impl_core_array_iter_IntoIter_N_T.
    
    Module Impl_core_iter_traits_iterator_Iterator_for_core_array_iter_IntoIter_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ].
      
      (*     type Item = T; *)
      Definition _Item (N : Value.t) (T : Ty.t) : Ty.t := T.
      
      (*
          fn next(&mut self) -> Option<Self::Item> {
              // Get the next index from the front.
              //
              // Increasing `alive.start` by 1 maintains the invariant regarding
              // `alive`. However, due to this change, for a short time, the alive
              // zone is not `data[alive]` anymore, but `data[idx..alive.end]`.
              self.alive.next().map(|idx| {
                  // Read the element from the array.
                  // SAFETY: `idx` is an index into the former "alive" region of the
                  // array. Reading this element means that `data[idx]` is regarded as
                  // dead now (i.e. do not touch). As `idx` was the start of the
                  // alive-zone, the alive zone is now `data[alive]` again, restoring
                  // all invariants.
                  unsafe { self.data.get_unchecked(idx).assume_init_read() }
              })
          }
      *)
      Definition next
          (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_associated_function (|
                Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                "map",
                [ T; Ty.function [ Ty.tuple [ Ty.path "usize" ] ] T ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    Ty.path "core::ops::index_range::IndexRange",
                    [],
                    "next",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::array::iter::IntoIter",
                      "alive"
                    |)
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let idx := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                        []
                                        [ T ],
                                      "assume_init_read",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "slice")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                                []
                                                [ T ]
                                            ],
                                          "get_unchecked",
                                          [ Ty.path "usize" ]
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::array::iter::IntoIter",
                                            "data"
                                          |);
                                          M.read (| idx |)
                                        ]
                                      |)
                                    ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn size_hint(&self) -> (usize, Option<usize>) {
              let len = self.len();
              (len, Some(len))
          }
      *)
      Definition size_hint
          (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.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::exact_size::ExactSizeIterator",
                      Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ],
                      [],
                      "len",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (|
                Value.Tuple
                  [
                    M.read (| len |);
                    Value.StructTuple "core::option::Option::Some" [ M.read (| len |) ]
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn fold<Acc, Fold>(mut self, init: Acc, mut fold: Fold) -> Acc
          where
              Fold: FnMut(Acc, Self::Item) -> Acc,
          {
              let data = &mut self.data;
              iter::ByRefSized(&mut self.alive).fold(init, |acc, idx| {
                  // SAFETY: idx is obtained by folding over the `alive` range, which implies the
                  // value is currently considered alive but as the range is being consumed each value
                  // we read here will only be read once and then considered dead.
                  fold(acc, unsafe { data.get_unchecked(idx).assume_init_read() })
              })
          }
      *)
      Definition fold
          (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
        | [], [ Acc; Fold ], [ self; init; fold ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let init := M.alloc (| init |) in
            let fold := M.alloc (| fold |) in
            M.read (|
              let~ data :=
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::array::iter::IntoIter",
                    "data"
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    Ty.apply
                      (Ty.path "core::iter::adapters::by_ref_sized::ByRefSized")
                      []
                      [ Ty.path "core::ops::index_range::IndexRange" ],
                    [],
                    "fold",
                    [ Acc; Ty.function [ Ty.tuple [ Acc; Ty.path "usize" ] ] Acc ]
                  |),
                  [
                    Value.StructTuple
                      "core::iter::adapters::by_ref_sized::ByRefSized"
                      [
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::array::iter::IntoIter",
                          "alive"
                        |)
                      ];
                    M.read (| init |);
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0; α1 ] =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| α0 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let acc := M.copy (| γ |) in
                                      M.match_operator (|
                                        M.alloc (| α1 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let idx := M.copy (| γ |) in
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::function::FnMut",
                                                  Fold,
                                                  [ Ty.tuple [ Acc; T ] ],
                                                  "call_mut",
                                                  []
                                                |),
                                                [
                                                  fold;
                                                  Value.Tuple
                                                    [
                                                      M.read (| acc |);
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path
                                                              "core::mem::maybe_uninit::MaybeUninit")
                                                            []
                                                            [ T ],
                                                          "assume_init_read",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.apply
                                                                (Ty.path "slice")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::mem::maybe_uninit::MaybeUninit")
                                                                    []
                                                                    [ T ]
                                                                ],
                                                              "get_unchecked",
                                                              [ Ty.path "usize" ]
                                                            |),
                                                            [ M.read (| data |); M.read (| idx |) ]
                                                          |)
                                                        ]
                                                      |)
                                                    ]
                                                ]
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn count(self) -> usize {
              self.len()
          }
      *)
      Definition count
          (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_trait_method (|
                "core::iter::traits::exact_size::ExactSizeIterator",
                Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ],
                [],
                "len",
                []
              |),
              [ self ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn last(mut self) -> Option<Self::Item> {
              self.next_back()
          }
      *)
      Definition last
          (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_trait_method (|
                "core::iter::traits::double_ended::DoubleEndedIterator",
                Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ],
                [],
                "next_back",
                []
              |),
              [ self ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
              // This also moves the start, which marks them as conceptually "dropped",
              // so if anything goes bad then our drop impl won't double-free them.
              let range_to_drop = self.alive.take_prefix(n);
              let remaining = n - range_to_drop.len();
      
              // SAFETY: These elements are currently initialized, so it's fine to drop them.
              unsafe {
                  let slice = self.data.get_unchecked_mut(range_to_drop);
                  ptr::drop_in_place(MaybeUninit::slice_assume_init_mut(slice));
              }
      
              NonZero::new(remaining).map_or(Ok(()), Err)
          }
      *)
      Definition advance_by
          (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; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ range_to_drop :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::ops::index_range::IndexRange",
                      "take_prefix",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::array::iter::IntoIter",
                        "alive"
                      |);
                      M.read (| n |)
                    ]
                  |)
                |) in
              let~ remaining :=
                M.alloc (|
                  BinOp.Wrap.sub (|
                    M.read (| n |),
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::ops::index_range::IndexRange",
                        "len",
                        []
                      |),
                      [ range_to_drop ]
                    |)
                  |)
                |) in
              let~ _ :=
                let~ slice :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "slice")
                          []
                          [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                        "get_unchecked_mut",
                        [ Ty.path "core::ops::index_range::IndexRange" ]
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::array::iter::IntoIter",
                          "data"
                        |);
                        M.read (| range_to_drop |)
                      ]
                    |)
                  |) 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 (| slice |) ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ],
                    "map_or",
                    [
                      Ty.apply
                        (Ty.path "core::result::Result")
                        []
                        [
                          Ty.tuple [];
                          Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                        ];
                      Ty.function
                        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ]
                        (Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [
                            Ty.tuple [];
                            Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                          ])
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                        "new",
                        []
                      |),
                      [ M.read (| remaining |) ]
                    |);
                    Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ];
                    M.constructor_as_closure "core::result::Result::Err"
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
              // SAFETY: The caller must provide an idx that is in bound of the remainder.
              unsafe { self.data.as_ptr().add(self.alive.start()).add(idx).cast::<T>().read() }
          }
      *)
      Definition __iterator_get_unchecked
          (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; idx ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let idx := M.alloc (| idx |) in
            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 "*const")
                      []
                      [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                    "cast",
                    [ T ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "*const")
                          []
                          [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                        "add",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "*const")
                              []
                              [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                              ],
                            "add",
                            []
                          |),
                          [
                            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.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::array::iter::IntoIter",
                                  "data"
                                |)
                              ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ops::index_range::IndexRange",
                                "start",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::array::iter::IntoIter",
                                  "alive"
                                |)
                              ]
                            |)
                          ]
                        |);
                        M.read (| idx |)
                      ]
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          (Self N T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item N T));
            ("next", InstanceField.Method (next N T));
            ("size_hint", InstanceField.Method (size_hint N T));
            ("fold", InstanceField.Method (fold N T));
            ("count", InstanceField.Method (count N T));
            ("last", InstanceField.Method (last N T));
            ("advance_by", InstanceField.Method (advance_by N T));
            ("__iterator_get_unchecked", InstanceField.Method (__iterator_get_unchecked N T))
          ].
    End Impl_core_iter_traits_iterator_Iterator_for_core_array_iter_IntoIter_N_T.
    
    Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_array_iter_IntoIter_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ].
      
      (*
          fn next_back(&mut self) -> Option<Self::Item> {
              // Get the next index from the back.
              //
              // Decreasing `alive.end` by 1 maintains the invariant regarding
              // `alive`. However, due to this change, for a short time, the alive
              // zone is not `data[alive]` anymore, but `data[alive.start..=idx]`.
              self.alive.next_back().map(|idx| {
                  // Read the element from the array.
                  // SAFETY: `idx` is an index into the former "alive" region of the
                  // array. Reading this element means that `data[idx]` is regarded as
                  // dead now (i.e. do not touch). As `idx` was the end of the
                  // alive-zone, the alive zone is now `data[alive]` again, restoring
                  // all invariants.
                  unsafe { self.data.get_unchecked(idx).assume_init_read() }
              })
          }
      *)
      Definition next_back
          (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_associated_function (|
                Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                "map",
                [ T; Ty.function [ Ty.tuple [ Ty.path "usize" ] ] T ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::double_ended::DoubleEndedIterator",
                    Ty.path "core::ops::index_range::IndexRange",
                    [],
                    "next_back",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::array::iter::IntoIter",
                      "alive"
                    |)
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let idx := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                        []
                                        [ T ],
                                      "assume_init_read",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "slice")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                                []
                                                [ T ]
                                            ],
                                          "get_unchecked",
                                          [ Ty.path "usize" ]
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::array::iter::IntoIter",
                                            "data"
                                          |);
                                          M.read (| idx |)
                                        ]
                                      |)
                                    ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn rfold<Acc, Fold>(mut self, init: Acc, mut rfold: Fold) -> Acc
          where
              Fold: FnMut(Acc, Self::Item) -> Acc,
          {
              let data = &mut self.data;
              iter::ByRefSized(&mut self.alive).rfold(init, |acc, idx| {
                  // SAFETY: idx is obtained by folding over the `alive` range, which implies the
                  // value is currently considered alive but as the range is being consumed each value
                  // we read here will only be read once and then considered dead.
                  rfold(acc, unsafe { data.get_unchecked(idx).assume_init_read() })
              })
          }
      *)
      Definition rfold
          (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
        | [], [ Acc; Fold ], [ self; init; rfold ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let init := M.alloc (| init |) in
            let rfold := M.alloc (| rfold |) in
            M.read (|
              let~ data :=
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::array::iter::IntoIter",
                    "data"
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::double_ended::DoubleEndedIterator",
                    Ty.apply
                      (Ty.path "core::iter::adapters::by_ref_sized::ByRefSized")
                      []
                      [ Ty.path "core::ops::index_range::IndexRange" ],
                    [],
                    "rfold",
                    [ Acc; Ty.function [ Ty.tuple [ Acc; Ty.path "usize" ] ] Acc ]
                  |),
                  [
                    Value.StructTuple
                      "core::iter::adapters::by_ref_sized::ByRefSized"
                      [
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::array::iter::IntoIter",
                          "alive"
                        |)
                      ];
                    M.read (| init |);
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0; α1 ] =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| α0 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let acc := M.copy (| γ |) in
                                      M.match_operator (|
                                        M.alloc (| α1 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let idx := M.copy (| γ |) in
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::function::FnMut",
                                                  Fold,
                                                  [ Ty.tuple [ Acc; T ] ],
                                                  "call_mut",
                                                  []
                                                |),
                                                [
                                                  rfold;
                                                  Value.Tuple
                                                    [
                                                      M.read (| acc |);
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path
                                                              "core::mem::maybe_uninit::MaybeUninit")
                                                            []
                                                            [ T ],
                                                          "assume_init_read",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.apply
                                                                (Ty.path "slice")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::mem::maybe_uninit::MaybeUninit")
                                                                    []
                                                                    [ T ]
                                                                ],
                                                              "get_unchecked",
                                                              [ Ty.path "usize" ]
                                                            |),
                                                            [ M.read (| data |); M.read (| idx |) ]
                                                          |)
                                                        ]
                                                      |)
                                                    ]
                                                ]
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
              // This also moves the end, which marks them as conceptually "dropped",
              // so if anything goes bad then our drop impl won't double-free them.
              let range_to_drop = self.alive.take_suffix(n);
              let remaining = n - range_to_drop.len();
      
              // SAFETY: These elements are currently initialized, so it's fine to drop them.
              unsafe {
                  let slice = self.data.get_unchecked_mut(range_to_drop);
                  ptr::drop_in_place(MaybeUninit::slice_assume_init_mut(slice));
              }
      
              NonZero::new(remaining).map_or(Ok(()), Err)
          }
      *)
      Definition advance_back_by
          (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; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ range_to_drop :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::ops::index_range::IndexRange",
                      "take_suffix",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::array::iter::IntoIter",
                        "alive"
                      |);
                      M.read (| n |)
                    ]
                  |)
                |) in
              let~ remaining :=
                M.alloc (|
                  BinOp.Wrap.sub (|
                    M.read (| n |),
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::ops::index_range::IndexRange",
                        "len",
                        []
                      |),
                      [ range_to_drop ]
                    |)
                  |)
                |) in
              let~ _ :=
                let~ slice :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "slice")
                          []
                          [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                        "get_unchecked_mut",
                        [ Ty.path "core::ops::index_range::IndexRange" ]
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::array::iter::IntoIter",
                          "data"
                        |);
                        M.read (| range_to_drop |)
                      ]
                    |)
                  |) 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 (| slice |) ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ],
                    "map_or",
                    [
                      Ty.apply
                        (Ty.path "core::result::Result")
                        []
                        [
                          Ty.tuple [];
                          Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                        ];
                      Ty.function
                        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ]
                        (Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [
                            Ty.tuple [];
                            Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                          ])
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                        "new",
                        []
                      |),
                      [ M.read (| remaining |) ]
                    |);
                    Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ];
                    M.constructor_as_closure "core::result::Result::Err"
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::double_ended::DoubleEndedIterator"
          (Self N T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("next_back", InstanceField.Method (next_back N T));
            ("rfold", InstanceField.Method (rfold N T));
            ("advance_back_by", InstanceField.Method (advance_back_by N T))
          ].
    End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_array_iter_IntoIter_N_T.
    
    Module Impl_core_ops_drop_Drop_for_core_array_iter_IntoIter_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ].
      
      (*
          fn drop(&mut self) {
              // SAFETY: This is safe: `as_mut_slice` returns exactly the sub-slice
              // of elements that have not been moved out yet and that remain
              // to be dropped.
              unsafe { ptr::drop_in_place(self.as_mut_slice()) }
          }
      *)
      Definition drop
          (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::ptr::drop_in_place",
                [ Ty.apply (Ty.path "slice") [] [ T ] ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ],
                    "as_mut_slice",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T : Ty.t),
        M.IsTraitInstance
          "core::ops::drop::Drop"
          (Self N T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("drop", InstanceField.Method (drop N T)) ].
    End Impl_core_ops_drop_Drop_for_core_array_iter_IntoIter_N_T.
    
    Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_array_iter_IntoIter_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ].
      
      (*
          fn len(&self) -> usize {
              self.alive.len()
          }
      *)
      Definition len
          (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_associated_function (|
                Ty.path "core::ops::index_range::IndexRange",
                "len",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::array::iter::IntoIter",
                  "alive"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn is_empty(&self) -> bool {
              self.alive.is_empty()
          }
      *)
      Definition is_empty
          (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_trait_method (|
                "core::iter::traits::exact_size::ExactSizeIterator",
                Ty.path "core::ops::index_range::IndexRange",
                [],
                "is_empty",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::array::iter::IntoIter",
                  "alive"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::exact_size::ExactSizeIterator"
          (Self N T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("len", InstanceField.Method (len N T));
            ("is_empty", InstanceField.Method (is_empty N T))
          ].
    End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_array_iter_IntoIter_N_T.
    
    Module Impl_core_iter_traits_marker_FusedIterator_for_core_array_iter_IntoIter_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ].
      
      Axiom Implements :
        forall (N : Value.t) (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          (Self N T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_for_core_array_iter_IntoIter_N_T.
    
    Module Impl_core_iter_traits_marker_TrustedLen_for_core_array_iter_IntoIter_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ].
      
      Axiom Implements :
        forall (N : Value.t) (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::TrustedLen"
          (Self N T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_TrustedLen_for_core_array_iter_IntoIter_N_T.
    
    (* Trait *)
    (* Empty module 'NonDrop' *)
    
    Module Impl_core_array_iter_NonDrop_where_core_marker_Copy_T_for_T.
      Definition Self (T : Ty.t) : Ty.t := T.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::array::iter::NonDrop"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_array_iter_NonDrop_where_core_marker_Copy_T_for_T.
    
    Module Impl_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_where_core_array_iter_NonDrop_T_for_core_array_iter_IntoIter_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ].
      
      (*     const MAY_HAVE_SIDE_EFFECT: bool = false; *)
      (* Ty.path "bool" *)
      Definition value_MAY_HAVE_SIDE_EFFECT (N : Value.t) (T : Ty.t) : Value.t :=
        let Self : Ty.t := Self N T in
        M.run ltac:(M.monadic (M.alloc (| Value.Bool false |))).
      
      Axiom Implements :
        forall (N : Value.t) (T : Ty.t),
        M.IsTraitInstance
          "core::iter::adapters::zip::TrustedRandomAccessNoCoerce"
          (Self N T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("value_MAY_HAVE_SIDE_EFFECT", InstanceField.Constant (value_MAY_HAVE_SIDE_EFFECT N T))
          ].
    End Impl_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_where_core_array_iter_NonDrop_T_for_core_array_iter_IntoIter_N_T.
    
    Module Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_array_iter_IntoIter_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ].
      
      (*
          fn clone(&self) -> Self {
              // Note, we don't really need to match the exact same alive range, so
              // we can just clone into offset 0 regardless of where `self` is.
              let mut new =
                  Self { data: [const { MaybeUninit::uninit() }; N], alive: IndexRange::zero_to(0) };
      
              // Clone all alive elements.
              for (src, dst) in iter::zip(self.as_slice(), &mut new.data) {
                  // Write a clone into the new array, then update its alive range.
                  // If cloning panics, we'll correctly drop the previous items.
                  dst.write(src.clone());
                  // This addition cannot overflow as we're iterating a slice
                  new.alive = IndexRange::zero_to(new.alive.end() + 1);
              }
      
              new
          }
      *)
      Definition clone
          (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.read (|
              let~ new :=
                M.alloc (|
                  Value.StructRecord
                    "core::array::iter::IntoIter"
                    [
                      ("data",
                        repeat (|
                          M.read (| M.get_constant (| "core::array::iter::clone_discriminant" |) |),
                          N
                        |));
                      ("alive",
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::ops::index_range::IndexRange",
                            "zero_to",
                            []
                          |),
                          [ 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::Iter") [] [ T ];
                              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_function (|
                              "core::iter::adapters::zip::zip",
                              [
                                Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ];
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "array")
                                      [ N ]
                                      [
                                        Ty.apply
                                          (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                          []
                                          [ T ]
                                      ]
                                  ]
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ],
                                  "as_slice",
                                  []
                                |),
                                [ M.read (| self |) ]
                              |);
                              M.SubPointer.get_struct_record_field (|
                                new,
                                "core::array::iter::IntoIter",
                                "data"
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::Iter") [] [ T ];
                                            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 γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                        let src := M.copy (| γ1_0 |) in
                                        let dst := 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 (| dst |);
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::clone::Clone",
                                                    T,
                                                    [],
                                                    "clone",
                                                    []
                                                  |),
                                                  [ M.read (| src |) ]
                                                |)
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              new,
                                              "core::array::iter::IntoIter",
                                              "alive"
                                            |),
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::ops::index_range::IndexRange",
                                                "zero_to",
                                                []
                                              |),
                                              [
                                                BinOp.Wrap.add (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "core::ops::index_range::IndexRange",
                                                      "end",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        new,
                                                        "core::array::iter::IntoIter",
                                                        "alive"
                                                      |)
                                                    ]
                                                  |),
                                                  Value.Integer IntegerKind.Usize 1
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) in
              new
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T : Ty.t),
        M.IsTraitInstance
          "core::clone::Clone"
          (Self N T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method (clone N T)) ].
    End Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_array_iter_IntoIter_N_T.
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_array_iter_IntoIter_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ].
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              // Only print the elements that were not yielded yet: we cannot
              // access the yielded elements anymore.
              f.debug_tuple("IntoIter").field(&self.as_slice()).finish()
          }
      *)
      Definition fmt
          (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; 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::builders::DebugTuple",
                "finish",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugTuple",
                    "field",
                    []
                  |),
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "IntoIter" |) ]
                      |)
                    |);
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ],
                          "as_slice",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self N T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt N T)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_array_iter_IntoIter_N_T.
  End iter.
End array.
