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

Module slice.
  Module iter.
    Module Impl_core_slice_iter_Iter_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ].
      
      (*
                  unsafe fn next_back_unchecked(&mut self) -> $elem {
                      // SAFETY: the caller promised it's not empty, so
                      // the offsetting is in-bounds and there's an element to return.
                      unsafe { self.pre_dec_end(1).$into_ref() }
                  }
      *)
      Definition next_back_unchecked
          (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_associated_function (|
                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                "as_ref",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                      "pre_dec_end",
                      []
                    |),
                    [ M.read (| self |); Value.Integer IntegerKind.Usize 1 ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_next_back_unchecked :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "next_back_unchecked" (next_back_unchecked T).
      
      (*
                  fn make_slice(&self) -> &'a [T] {
                      // SAFETY: the iterator was created from a slice with pointer
                      // `self.ptr` and length `len!(self)`. This guarantees that all
                      // the prerequisites for `from_raw_parts` are fulfilled.
                      unsafe { from_raw_parts(self.ptr.as_ptr(), len!(self)) }
                  }
      *)
      Definition make_slice (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", [ T ] |),
              [
                (* MutToConstPointer *)
                M.pointer_coercion
                  (M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::slice::iter::Iter",
                          "ptr"
                        |)
                      |)
                    ]
                  |));
                M.read (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ len :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*const") [] [ T ],
                                  "addr",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::slice::iter::Iter",
                                      "end_or_len"
                                    |)
                                  |)
                                ]
                              |)
                            |) in
                          len));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ end_ :=
                            M.copy (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "*const")
                                    []
                                    [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                  "cast",
                                  [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::Iter",
                                    "end_or_len"
                                  |)
                                ]
                              |)
                            |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                "sub_ptr",
                                []
                              |),
                              [
                                M.read (| end_ |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::Iter",
                                    "ptr"
                                  |)
                                |)
                              ]
                            |)
                          |)))
                    ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_make_slice :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "make_slice" (make_slice T).
      
      (*
                  unsafe fn post_inc_start(&mut self, offset: usize) -> NonNull<T> {
                      let old = self.ptr;
      
                      // SAFETY: the caller guarantees that `offset` doesn't exceed `self.len()`,
                      // so this new pointer is inside `self` and thus guaranteed to be non-null.
                      unsafe {
                          if_zst!(mut self,
                              // Using the intrinsic directly avoids emitting a UbCheck
                              len => *len = crate::intrinsics::unchecked_sub( *len, offset),
                              _end => self.ptr = self.ptr.add(offset),
                          );
                      }
                      old
                  }
      *)
      Definition post_inc_start
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; offset ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let offset := M.alloc (| offset |) in
            M.read (|
              let~ old :=
                M.copy (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::slice::iter::Iter",
                    "ptr"
                  |)
                |) in
              let~ _ :=
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ len :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "*mut")
                                    []
                                    [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                  "cast",
                                  [ Ty.path "usize" ]
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::Iter",
                                    "end_or_len"
                                  |)
                                ]
                              |)
                            |) in
                          M.write (|
                            M.read (| len |),
                            M.call_closure (|
                              M.get_function (|
                                "core::intrinsics::unchecked_sub",
                                [ Ty.path "usize" ]
                              |),
                              [ M.read (| M.read (| len |) |); M.read (| offset |) ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ _end :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "*mut")
                                    []
                                    [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                  "cast",
                                  [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::Iter",
                                    "end_or_len"
                                  |)
                                ]
                              |)
                            |) in
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::slice::iter::Iter",
                              "ptr"
                            |),
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                "add",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::Iter",
                                    "ptr"
                                  |)
                                |);
                                M.read (| offset |)
                              ]
                            |)
                          |)))
                    ]
                  |) in
                M.alloc (| Value.Tuple [] |) in
              old
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_post_inc_start :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "post_inc_start" (post_inc_start T).
      
      (*
                  unsafe fn pre_dec_end(&mut self, offset: usize) -> NonNull<T> {
                      if_zst!(mut self,
                          // SAFETY: By our precondition, `offset` can be at most the
                          // current length, so the subtraction can never overflow.
                          len => unsafe {
                              // Using the intrinsic directly avoids emitting a UbCheck
                              *len = crate::intrinsics::unchecked_sub( *len, offset);
                              self.ptr
                          },
                          // SAFETY: the caller guarantees that `offset` doesn't exceed `self.len()`,
                          // which is guaranteed to not overflow an `isize`. Also, the resulting pointer
                          // is in bounds of `slice`, which fulfills the other requirements for `offset`.
                          end => unsafe {
                              *end = end.sub(offset);
                              *end
                          },
                      )
                  }
      *)
      Definition pre_dec_end (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; offset ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let offset := M.alloc (| offset |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ len :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ Ty.apply (Ty.path "*const") [] [ T ] ],
                              "cast",
                              [ Ty.path "usize" ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::iter::Iter",
                                "end_or_len"
                              |)
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.write (|
                          M.read (| len |),
                          M.call_closure (|
                            M.get_function (|
                              "core::intrinsics::unchecked_sub",
                              [ Ty.path "usize" ]
                            |),
                            [ M.read (| M.read (| len |) |); M.read (| offset |) ]
                          |)
                        |) in
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::slice::iter::Iter",
                        "ptr"
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let~ end_ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ Ty.apply (Ty.path "*const") [] [ T ] ],
                              "cast",
                              [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::iter::Iter",
                                "end_or_len"
                              |)
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.write (|
                          M.read (| end_ |),
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                              "sub",
                              []
                            |),
                            [ M.read (| M.read (| end_ |) |); M.read (| offset |) ]
                          |)
                        |) in
                      M.read (| end_ |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_pre_dec_end :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "pre_dec_end" (pre_dec_end T).
    End Impl_core_slice_iter_Iter_T.
    
    Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_slice_iter_Iter_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ].
      
      (*
                  fn len(&self) -> usize {
                      len!(self)
                  }
      *)
      Definition len (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ len :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*const") [] [ T ],
                              "addr",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::slice::iter::Iter",
                                  "end_or_len"
                                |)
                              |)
                            ]
                          |)
                        |) in
                      len));
                  fun γ =>
                    ltac:(M.monadic
                      (let~ end_ :=
                        M.copy (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "*const")
                                []
                                [ Ty.apply (Ty.path "*const") [] [ T ] ],
                              "cast",
                              [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::iter::Iter",
                                "end_or_len"
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            "sub_ptr",
                            []
                          |),
                          [
                            M.read (| end_ |);
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::iter::Iter",
                                "ptr"
                              |)
                            |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn is_empty(&self) -> bool {
                      is_empty!(self)
                  }
      *)
      Definition is_empty (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ len :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*const") [] [ T ],
                              "addr",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::slice::iter::Iter",
                                  "end_or_len"
                                |)
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (|
                        BinOp.eq (| M.read (| len |), Value.Integer IntegerKind.Usize 0 |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let~ end_ :=
                        M.copy (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "*const")
                                []
                                [ Ty.apply (Ty.path "*const") [] [ T ] ],
                              "cast",
                              [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::iter::Iter",
                                "end_or_len"
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ],
                            "eq",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::slice::iter::Iter",
                              "ptr"
                            |);
                            end_
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::exact_size::ExactSizeIterator"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("len", InstanceField.Method (len T)); ("is_empty", InstanceField.Method (is_empty T))
          ].
    End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_slice_iter_Iter_T.
    
    Module Impl_core_iter_traits_iterator_Iterator_for_core_slice_iter_Iter_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ].
      
      (*             type Item = $elem; *)
      Definition _Item (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
      
      (*
                  fn next(&mut self) -> Option<$elem> {
                      // could be implemented with slices, but this avoids bounds checks
      
                      // SAFETY: The call to `next_unchecked` is
                      // safe since we check if the iterator is empty first.
                      unsafe {
                          if is_empty!(self) {
                              None
                          } else {
                              Some(self.next_unchecked())
                          }
                      }
                  }
      *)
      Definition next (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.get_constant (|
                                        "core::mem::SizedTypeProperties::IS_ZST"
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ len :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "*const") [] [ T ],
                                          "addr",
                                          []
                                        |),
                                        [
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "core::slice::iter::Iter",
                                              "end_or_len"
                                            |)
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (|
                                    BinOp.eq (|
                                      M.read (| len |),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let~ end_ :=
                                    M.copy (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "*const")
                                            []
                                            [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                          "cast",
                                          [
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ T ]
                                          ]
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::slice::iter::Iter",
                                            "end_or_len"
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                        [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ]
                                        ],
                                        "eq",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::Iter",
                                          "ptr"
                                        |);
                                        end_
                                      ]
                                    |)
                                  |)))
                            ]
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::unchecked_iterator::UncheckedIterator",
                                Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                [],
                                "next_unchecked",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn size_hint(&self) -> (usize, Option<usize>) {
                      let exact = len!(self);
                      (exact, Some(exact))
                  }
      *)
      Definition size_hint (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~ exact :=
                M.copy (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ len :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*const") [] [ T ],
                                  "addr",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::slice::iter::Iter",
                                      "end_or_len"
                                    |)
                                  |)
                                ]
                              |)
                            |) in
                          len));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ end_ :=
                            M.copy (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "*const")
                                    []
                                    [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                  "cast",
                                  [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::Iter",
                                    "end_or_len"
                                  |)
                                ]
                              |)
                            |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                "sub_ptr",
                                []
                              |),
                              [
                                M.read (| end_ |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::Iter",
                                    "ptr"
                                  |)
                                |)
                              ]
                            |)
                          |)))
                    ]
                  |)
                |) in
              M.alloc (|
                Value.Tuple
                  [
                    M.read (| exact |);
                    Value.StructTuple "core::option::Option::Some" [ M.read (| exact |) ]
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn count(self) -> usize {
                      len!(self)
                  }
      *)
      Definition count (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ len :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*const") [] [ T ],
                              "addr",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::slice::iter::Iter",
                                  "end_or_len"
                                |)
                              |)
                            ]
                          |)
                        |) in
                      len));
                  fun γ =>
                    ltac:(M.monadic
                      (let~ end_ :=
                        M.copy (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "*const")
                                []
                                [ Ty.apply (Ty.path "*const") [] [ T ] ],
                              "cast",
                              [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                self,
                                "core::slice::iter::Iter",
                                "end_or_len"
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            "sub_ptr",
                            []
                          |),
                          [
                            M.read (| end_ |);
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                self,
                                "core::slice::iter::Iter",
                                "ptr"
                              |)
                            |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn nth(&mut self, n: usize) -> Option<$elem> {
                      if n >= len!(self) {
                          // This iterator is now empty.
                          if_zst!(mut self,
                              len => *len = 0,
                              end => self.ptr = *end,
                          );
                          return None;
                      }
                      // SAFETY: We are in bounds. `post_inc_start` does the right thing even for ZSTs.
                      unsafe {
                          self.post_inc_start(n);
                          Some(self.next_unchecked())
                      }
                  }
      *)
      Definition nth (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ge (|
                                    M.read (| n |),
                                    M.read (|
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.get_constant (|
                                                    "core::mem::SizedTypeProperties::IS_ZST"
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              let~ len :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply (Ty.path "*const") [] [ T ],
                                                      "addr",
                                                      []
                                                    |),
                                                    [
                                                      M.read (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "core::slice::iter::Iter",
                                                          "end_or_len"
                                                        |)
                                                      |)
                                                    ]
                                                  |)
                                                |) in
                                              len));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let~ end_ :=
                                                M.copy (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "*const")
                                                        []
                                                        [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                                      "cast",
                                                      [
                                                        Ty.apply
                                                          (Ty.path "core::ptr::non_null::NonNull")
                                                          []
                                                          [ T ]
                                                      ]
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "core::slice::iter::Iter",
                                                        "end_or_len"
                                                      |)
                                                    ]
                                                  |)
                                                |) in
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "core::ptr::non_null::NonNull")
                                                      []
                                                      [ T ],
                                                    "sub_ptr",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| end_ |);
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "core::slice::iter::Iter",
                                                        "ptr"
                                                      |)
                                                    |)
                                                  ]
                                                |)
                                              |)))
                                        ]
                                      |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.get_constant (|
                                                  "core::mem::SizedTypeProperties::IS_ZST"
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            let~ len :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "*mut")
                                                      []
                                                      [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                                    "cast",
                                                    [ Ty.path "usize" ]
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "core::slice::iter::Iter",
                                                      "end_or_len"
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.write (|
                                              M.read (| len |),
                                              Value.Integer IntegerKind.Usize 0
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let~ end_ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "*mut")
                                                      []
                                                      [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                                    "cast",
                                                    [
                                                      Ty.apply
                                                        (Ty.path "core::ptr::non_null::NonNull")
                                                        []
                                                        [ T ]
                                                    ]
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "core::slice::iter::Iter",
                                                      "end_or_len"
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.write (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "core::slice::iter::Iter",
                                                "ptr"
                                              |),
                                              M.read (| M.read (| end_ |) |)
                                            |)))
                                      ]
                                    |) in
                                  M.return_ (| Value.StructTuple "core::option::Option::None" [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                          "post_inc_start",
                          []
                        |),
                        [ M.read (| self |); M.read (| n |) ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::unchecked_iterator::UncheckedIterator",
                            Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                            [],
                            "next_unchecked",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                      let advance = cmp::min(len!(self), n);
                      // SAFETY: By construction, `advance` does not exceed `self.len()`.
                      unsafe { self.post_inc_start(advance) };
                      NonZero::new(n - advance).map_or(Ok(()), Err)
                  }
      *)
      Definition advance_by (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ advance :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::cmp::min", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.get_constant (|
                                      "core::mem::SizedTypeProperties::IS_ZST"
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ len :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "*const") [] [ T ],
                                        "addr",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::slice::iter::Iter",
                                            "end_or_len"
                                          |)
                                        |)
                                      ]
                                    |)
                                  |) in
                                len));
                            fun γ =>
                              ltac:(M.monadic
                                (let~ end_ :=
                                  M.copy (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "*const")
                                          []
                                          [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                        "cast",
                                        [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ]
                                        ]
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::Iter",
                                          "end_or_len"
                                        |)
                                      ]
                                    |)
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                      "sub_ptr",
                                      []
                                    |),
                                    [
                                      M.read (| end_ |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::Iter",
                                          "ptr"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)))
                          ]
                        |)
                      |);
                      M.read (| n |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                      "post_inc_start",
                      []
                    |),
                    [ M.read (| self |); M.read (| advance |) ]
                  |)
                |) 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",
                        []
                      |),
                      [ BinOp.Wrap.sub (| M.read (| n |), M.read (| advance |) |) ]
                    |);
                    Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ];
                    M.constructor_as_closure "core::result::Result::Err"
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn last(mut self) -> Option<$elem> {
                      self.next_back()
                  }
      *)
      Definition last (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_trait_method (|
                "core::iter::traits::double_ended::DoubleEndedIterator",
                Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                [],
                "next_back",
                []
              |),
              [ self ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn fold<B, F>(self, init: B, mut f: F) -> B
                      where
                          F: FnMut(B, Self::Item) -> B,
                  {
                      // this implementation consists of the following optimizations compared to the
                      // default implementation:
                      // - do-while loop, as is llvm's preferred loop shape,
                      //   see https://releases.llvm.org/16.0.0/docs/LoopTerminology.html#more-canonical-loops
                      // - bumps an index instead of a pointer since the latter case inhibits
                      //   some optimizations, see #111603
                      // - avoids Option wrapping/matching
                      if is_empty!(self) {
                          return init;
                      }
                      let mut acc = init;
                      let mut i = 0;
                      let len = len!(self);
                      loop {
                          // SAFETY: the loop iterates `i in 0..len`, which always is in bounds of
                          // the slice allocation
                          acc = f(acc, unsafe { & $( $mut_ )? *self.ptr.add(i).as_ptr() });
                          // SAFETY: `i` can't overflow since it'll only reach usize::MAX if the
                          // slice had that length, in which case we'll break out of the loop
                          // after the increment
                          i = unsafe { i.unchecked_add(1) };
                          if i == len {
                              break;
                          }
                      }
                      acc
                  }
      *)
      Definition fold (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ B; F ], [ self; init; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let init := M.alloc (| init |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.get_constant (|
                                              "core::mem::SizedTypeProperties::IS_ZST"
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ len :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*const") [] [ T ],
                                                "addr",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    self,
                                                    "core::slice::iter::Iter",
                                                    "end_or_len"
                                                  |)
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (|
                                          BinOp.eq (|
                                            M.read (| len |),
                                            Value.Integer IntegerKind.Usize 0
                                          |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let~ end_ :=
                                          M.copy (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "*const")
                                                  []
                                                  [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                                "cast",
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::ptr::non_null::NonNull")
                                                    []
                                                    [ T ]
                                                ]
                                              |),
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  self,
                                                  "core::slice::iter::Iter",
                                                  "end_or_len"
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::cmp::PartialEq",
                                              Ty.apply
                                                (Ty.path "core::ptr::non_null::NonNull")
                                                []
                                                [ T ],
                                              [
                                                Ty.apply
                                                  (Ty.path "core::ptr::non_null::NonNull")
                                                  []
                                                  [ T ]
                                              ],
                                              "eq",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                self,
                                                "core::slice::iter::Iter",
                                                "ptr"
                                              |);
                                              end_
                                            ]
                                          |)
                                        |)))
                                  ]
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| M.read (| init |) |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ acc := M.copy (| init |) in
                  let~ i := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                  let~ len :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ len :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ T ],
                                      "addr",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          self,
                                          "core::slice::iter::Iter",
                                          "end_or_len"
                                        |)
                                      |)
                                    ]
                                  |)
                                |) in
                              len));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ end_ :=
                                M.copy (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "*const")
                                        []
                                        [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                      "cast",
                                      [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        self,
                                        "core::slice::iter::Iter",
                                        "end_or_len"
                                      |)
                                    ]
                                  |)
                                |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                    "sub_ptr",
                                    []
                                  |),
                                  [
                                    M.read (| end_ |);
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        self,
                                        "core::slice::iter::Iter",
                                        "ptr"
                                      |)
                                    |)
                                  ]
                                |)
                              |)))
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (let~ _ :=
                          M.write (|
                            acc,
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::function::FnMut",
                                F,
                                [ Ty.tuple [ B; Ty.apply (Ty.path "&") [] [ T ] ] ],
                                "call_mut",
                                []
                              |),
                              [
                                f;
                                Value.Tuple
                                  [
                                    M.read (| acc |);
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                        "as_ptr",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ T ],
                                            "add",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                self,
                                                "core::slice::iter::Iter",
                                                "ptr"
                                              |)
                                            |);
                                            M.read (| i |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  ]
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.write (|
                            i,
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "usize", "unchecked_add", [] |),
                              [ M.read (| i |); Value.Integer IntegerKind.Usize 1 ]
                            |)
                          |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.eq (| M.read (| i |), M.read (| len |) |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |)))
                    |) in
                  acc
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn for_each<F>(mut self, mut f: F)
                  where
                      Self: Sized,
                      F: FnMut(Self::Item),
                  {
                      while let Some(x) = self.next() {
                          f(x);
                      }
                  }
      *)
      Definition for_each (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ F ], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              M.loop (|
                ltac:(M.monadic
                  (M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                  [],
                                  "next",
                                  []
                                |),
                                [ self ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let x := M.copy (| γ0_0 |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::function::FnMut",
                                  F,
                                  [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                                  "call_mut",
                                  []
                                |),
                                [ f; Value.Tuple [ M.read (| x |) ] ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                                M.alloc (| Value.Tuple [] |)
                              |)
                            |)
                          |)))
                    ]
                  |)))
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn all<F>(&mut self, mut f: F) -> bool
                  where
                      Self: Sized,
                      F: FnMut(Self::Item) -> bool,
                  {
                      while let Some(x) = self.next() {
                          if !f(x) {
                              return false;
                          }
                      }
                      true
                  }
      *)
      Definition all (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ F ], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let x := M.copy (| γ0_0 |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              UnOp.not (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::function::FnMut",
                                                    F,
                                                    [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ]
                                                    ],
                                                    "call_mut",
                                                    []
                                                  |),
                                                  [ f; Value.Tuple [ M.read (| x |) ] ]
                                                |)
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (| M.return_ (| Value.Bool false |) |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.alloc (| Value.Bool true |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn any<F>(&mut self, mut f: F) -> bool
                  where
                      Self: Sized,
                      F: FnMut(Self::Item) -> bool,
                  {
                      while let Some(x) = self.next() {
                          if f(x) {
                              return true;
                          }
                      }
                      false
                  }
      *)
      Definition any (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ F ], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let x := M.copy (| γ0_0 |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::function::FnMut",
                                                  F,
                                                  [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                                                  "call_mut",
                                                  []
                                                |),
                                                [ f; Value.Tuple [ M.read (| x |) ] ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (| M.return_ (| Value.Bool true |) |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.alloc (| Value.Bool false |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn find<P>(&mut self, mut predicate: P) -> Option<Self::Item>
                  where
                      Self: Sized,
                      P: FnMut(&Self::Item) -> bool,
                  {
                      while let Some(x) = self.next() {
                          if predicate(&x) {
                              return Some(x);
                          }
                      }
                      None
                  }
      *)
      Definition find (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ P ], [ self; predicate ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let predicate := M.alloc (| predicate |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let x := M.copy (| γ0_0 |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::function::FnMut",
                                                  P,
                                                  [
                                                    Ty.tuple
                                                      [
                                                        Ty.apply
                                                          (Ty.path "&")
                                                          []
                                                          [ Ty.apply (Ty.path "&") [] [ T ] ]
                                                      ]
                                                  ],
                                                  "call_mut",
                                                  []
                                                |),
                                                [ predicate; Value.Tuple [ x ] ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.return_ (|
                                                Value.StructTuple
                                                  "core::option::Option::Some"
                                                  [ M.read (| x |) ]
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn find_map<B, F>(&mut self, mut f: F) -> Option<B>
                  where
                      Self: Sized,
                      F: FnMut(Self::Item) -> Option<B>,
                  {
                      while let Some(x) = self.next() {
                          if let Some(y) = f(x) {
                              return Some(y);
                          }
                      }
                      None
                  }
      *)
      Definition find_map (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ B; F ], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let x := M.copy (| γ0_0 |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::function::FnMut",
                                                F,
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                                                "call_mut",
                                                []
                                              |),
                                              [ f; Value.Tuple [ M.read (| x |) ] ]
                                            |)
                                          |) in
                                        let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::option::Option::Some",
                                            0
                                          |) in
                                        let y := M.copy (| γ0_0 |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.return_ (|
                                                Value.StructTuple
                                                  "core::option::Option::Some"
                                                  [ M.read (| y |) ]
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn position<P>(&mut self, mut predicate: P) -> Option<usize> where
                      Self: Sized,
                      P: FnMut(Self::Item) -> bool,
                  {
                      let n = len!(self);
                      let mut i = 0;
                      while let Some(x) = self.next() {
                          if predicate(x) {
                              // SAFETY: we are guaranteed to be in bounds by the loop invariant:
                              // when `i >= n`, `self.next()` returns `None` and the loop breaks.
                              unsafe { assert_unchecked(i < n) };
                              return Some(i);
                          }
                          i += 1;
                      }
                      None
                  }
      *)
      Definition position (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ P ], [ self; predicate ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let predicate := M.alloc (| predicate |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ n :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ len :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ T ],
                                      "addr",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::Iter",
                                          "end_or_len"
                                        |)
                                      |)
                                    ]
                                  |)
                                |) in
                              len));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ end_ :=
                                M.copy (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "*const")
                                        []
                                        [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                      "cast",
                                      [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "core::slice::iter::Iter",
                                        "end_or_len"
                                      |)
                                    ]
                                  |)
                                |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                    "sub_ptr",
                                    []
                                  |),
                                  [
                                    M.read (| end_ |);
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "core::slice::iter::Iter",
                                        "ptr"
                                      |)
                                    |)
                                  ]
                                |)
                              |)))
                        ]
                      |)
                    |) in
                  let~ i := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let x := M.copy (| γ0_0 |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::function::FnMut",
                                                    P,
                                                    [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ]
                                                    ],
                                                    "call_mut",
                                                    []
                                                  |),
                                                  [ predicate; Value.Tuple [ M.read (| x |) ] ]
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ _ :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::hint::assert_unchecked",
                                                        []
                                                      |),
                                                      [
                                                        BinOp.lt (|
                                                          M.read (| i |),
                                                          M.read (| n |)
                                                        |)
                                                      ]
                                                    |)
                                                  |) in
                                                M.return_ (|
                                                  Value.StructTuple
                                                    "core::option::Option::Some"
                                                    [ M.read (| i |) ]
                                                |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                let~ _ :=
                                  let β := i in
                                  M.write (|
                                    β,
                                    BinOp.Wrap.add (|
                                      M.read (| β |),
                                      Value.Integer IntegerKind.Usize 1
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn rposition<P>(&mut self, mut predicate: P) -> Option<usize> where
                      P: FnMut(Self::Item) -> bool,
                      Self: Sized + ExactSizeIterator + DoubleEndedIterator
                  {
                      let n = len!(self);
                      let mut i = n;
                      while let Some(x) = self.next_back() {
                          i -= 1;
                          if predicate(x) {
                              // SAFETY: `i` must be lower than `n` since it starts at `n`
                              // and is only decreasing.
                              unsafe { assert_unchecked(i < n) };
                              return Some(i);
                          }
                      }
                      None
                  }
      *)
      Definition rposition (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ P ], [ self; predicate ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let predicate := M.alloc (| predicate |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ n :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ len :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ T ],
                                      "addr",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::Iter",
                                          "end_or_len"
                                        |)
                                      |)
                                    ]
                                  |)
                                |) in
                              len));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ end_ :=
                                M.copy (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "*const")
                                        []
                                        [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                      "cast",
                                      [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "core::slice::iter::Iter",
                                        "end_or_len"
                                      |)
                                    ]
                                  |)
                                |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                    "sub_ptr",
                                    []
                                  |),
                                  [
                                    M.read (| end_ |);
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "core::slice::iter::Iter",
                                        "ptr"
                                      |)
                                    |)
                                  ]
                                |)
                              |)))
                        ]
                      |)
                    |) in
                  let~ i := M.copy (| n |) in
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::double_ended::DoubleEndedIterator",
                                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                        [],
                                        "next_back",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let x := M.copy (| γ0_0 |) in
                                let~ _ :=
                                  let β := i in
                                  M.write (|
                                    β,
                                    BinOp.Wrap.sub (|
                                      M.read (| β |),
                                      Value.Integer IntegerKind.Usize 1
                                    |)
                                  |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::function::FnMut",
                                                  P,
                                                  [ Ty.tuple [ Ty.associated ] ],
                                                  "call_mut",
                                                  []
                                                |),
                                                [ predicate; Value.Tuple [ M.read (| x |) ] ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              let~ _ :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::hint::assert_unchecked",
                                                      []
                                                    |),
                                                    [ BinOp.lt (| M.read (| i |), M.read (| n |) |)
                                                    ]
                                                  |)
                                                |) in
                                              M.return_ (|
                                                Value.StructTuple
                                                  "core::option::Option::Some"
                                                  [ M.read (| i |) ]
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
                      // SAFETY: the caller must guarantee that `i` is in bounds of
                      // the underlying slice, so `i` cannot overflow an `isize`, and
                      // the returned references is guaranteed to refer to an element
                      // of the slice and thus guaranteed to be valid.
                      //
                      // Also note that the caller also guarantees that we're never
                      // called with the same index again, and that no other methods
                      // that will access this subslice are called, so it is valid
                      // for the returned reference to be mutable in the case of
                      // `IterMut`
                      unsafe { & $( $mut_ )? * self.ptr.as_ptr().add(idx) }
                  }
      *)
      Definition __iterator_get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self 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 "*mut") [] [ T ], "add", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::slice::iter::Iter",
                        "ptr"
                      |)
                    |)
                  ]
                |);
                M.read (| idx |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn is_sorted_by<F>(self, mut compare: F) -> bool
          where
              Self: Sized,
              F: FnMut(&Self::Item, &Self::Item) -> bool,
          {
              self.as_slice().is_sorted_by(|a, b| compare(&a, &b))
          }
      *)
      Definition is_sorted_by
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ F ], [ self; compare ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let compare := M.alloc (| compare |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "slice") [] [ T ],
                "is_sorted_by",
                [
                  Ty.function
                    [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ]
                    ]
                    (Ty.path "bool")
                ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                    "as_slice",
                    []
                  |),
                  [ self ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0; α1 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let a := M.copy (| γ |) in
                                  M.match_operator (|
                                    M.alloc (| α1 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let b := M.copy (| γ |) in
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::function::FnMut",
                                              F,
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.apply
                                                      (Ty.path "&")
                                                      []
                                                      [ Ty.apply (Ty.path "&") [] [ T ] ];
                                                    Ty.apply
                                                      (Ty.path "&")
                                                      []
                                                      [ Ty.apply (Ty.path "&") [] [ T ] ]
                                                  ]
                                              ],
                                              "call_mut",
                                              []
                                            |),
                                            [ compare; Value.Tuple [ a; b ] ]
                                          |)))
                                    ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item T));
            ("next", InstanceField.Method (next T));
            ("size_hint", InstanceField.Method (size_hint T));
            ("count", InstanceField.Method (count T));
            ("nth", InstanceField.Method (nth T));
            ("advance_by", InstanceField.Method (advance_by T));
            ("last", InstanceField.Method (last T));
            ("fold", InstanceField.Method (fold T));
            ("for_each", InstanceField.Method (for_each T));
            ("all", InstanceField.Method (all T));
            ("any", InstanceField.Method (any T));
            ("find", InstanceField.Method (find T));
            ("find_map", InstanceField.Method (find_map T));
            ("position", InstanceField.Method (position T));
            ("rposition", InstanceField.Method (rposition T));
            ("__iterator_get_unchecked", InstanceField.Method (__iterator_get_unchecked T));
            ("is_sorted_by", InstanceField.Method (is_sorted_by T))
          ].
    End Impl_core_iter_traits_iterator_Iterator_for_core_slice_iter_Iter_T.
    
    Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_slice_iter_Iter_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ].
      
      (*
                  fn next_back(&mut self) -> Option<$elem> {
                      // could be implemented with slices, but this avoids bounds checks
      
                      // SAFETY: The call to `next_back_unchecked`
                      // is safe since we check if the iterator is empty first.
                      unsafe {
                          if is_empty!(self) {
                              None
                          } else {
                              Some(self.next_back_unchecked())
                          }
                      }
                  }
      *)
      Definition next_back (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.get_constant (|
                                        "core::mem::SizedTypeProperties::IS_ZST"
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ len :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "*const") [] [ T ],
                                          "addr",
                                          []
                                        |),
                                        [
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "core::slice::iter::Iter",
                                              "end_or_len"
                                            |)
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (|
                                    BinOp.eq (|
                                      M.read (| len |),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let~ end_ :=
                                    M.copy (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "*const")
                                            []
                                            [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                          "cast",
                                          [
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ T ]
                                          ]
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::slice::iter::Iter",
                                            "end_or_len"
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                        [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ]
                                        ],
                                        "eq",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::Iter",
                                          "ptr"
                                        |);
                                        end_
                                      ]
                                    |)
                                  |)))
                            ]
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                "next_back_unchecked",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn nth_back(&mut self, n: usize) -> Option<$elem> {
                      if n >= len!(self) {
                          // This iterator is now empty.
                          if_zst!(mut self,
                              len => *len = 0,
                              end => *end = self.ptr,
                          );
                          return None;
                      }
                      // SAFETY: We are in bounds. `pre_dec_end` does the right thing even for ZSTs.
                      unsafe {
                          self.pre_dec_end(n);
                          Some(self.next_back_unchecked())
                      }
                  }
      *)
      Definition nth_back (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ge (|
                                    M.read (| n |),
                                    M.read (|
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.get_constant (|
                                                    "core::mem::SizedTypeProperties::IS_ZST"
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              let~ len :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply (Ty.path "*const") [] [ T ],
                                                      "addr",
                                                      []
                                                    |),
                                                    [
                                                      M.read (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "core::slice::iter::Iter",
                                                          "end_or_len"
                                                        |)
                                                      |)
                                                    ]
                                                  |)
                                                |) in
                                              len));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let~ end_ :=
                                                M.copy (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "*const")
                                                        []
                                                        [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                                      "cast",
                                                      [
                                                        Ty.apply
                                                          (Ty.path "core::ptr::non_null::NonNull")
                                                          []
                                                          [ T ]
                                                      ]
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "core::slice::iter::Iter",
                                                        "end_or_len"
                                                      |)
                                                    ]
                                                  |)
                                                |) in
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "core::ptr::non_null::NonNull")
                                                      []
                                                      [ T ],
                                                    "sub_ptr",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| end_ |);
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "core::slice::iter::Iter",
                                                        "ptr"
                                                      |)
                                                    |)
                                                  ]
                                                |)
                                              |)))
                                        ]
                                      |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.get_constant (|
                                                  "core::mem::SizedTypeProperties::IS_ZST"
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            let~ len :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "*mut")
                                                      []
                                                      [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                                    "cast",
                                                    [ Ty.path "usize" ]
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "core::slice::iter::Iter",
                                                      "end_or_len"
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.write (|
                                              M.read (| len |),
                                              Value.Integer IntegerKind.Usize 0
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let~ end_ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "*mut")
                                                      []
                                                      [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                                    "cast",
                                                    [
                                                      Ty.apply
                                                        (Ty.path "core::ptr::non_null::NonNull")
                                                        []
                                                        [ T ]
                                                    ]
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "core::slice::iter::Iter",
                                                      "end_or_len"
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.write (|
                                              M.read (| end_ |),
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "core::slice::iter::Iter",
                                                  "ptr"
                                                |)
                                              |)
                                            |)))
                                      ]
                                    |) in
                                  M.return_ (| Value.StructTuple "core::option::Option::None" [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                          "pre_dec_end",
                          []
                        |),
                        [ M.read (| self |); M.read (| n |) ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                            "next_back_unchecked",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                      let advance = cmp::min(len!(self), n);
                      // SAFETY: By construction, `advance` does not exceed `self.len()`.
                      unsafe { self.pre_dec_end(advance) };
                      NonZero::new(n - advance).map_or(Ok(()), Err)
                  }
      *)
      Definition advance_back_by
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ advance :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::cmp::min", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.get_constant (|
                                      "core::mem::SizedTypeProperties::IS_ZST"
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ len :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "*const") [] [ T ],
                                        "addr",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::slice::iter::Iter",
                                            "end_or_len"
                                          |)
                                        |)
                                      ]
                                    |)
                                  |) in
                                len));
                            fun γ =>
                              ltac:(M.monadic
                                (let~ end_ :=
                                  M.copy (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "*const")
                                          []
                                          [ Ty.apply (Ty.path "*const") [] [ T ] ],
                                        "cast",
                                        [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ]
                                        ]
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::Iter",
                                          "end_or_len"
                                        |)
                                      ]
                                    |)
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                      "sub_ptr",
                                      []
                                    |),
                                    [
                                      M.read (| end_ |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::Iter",
                                          "ptr"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)))
                          ]
                        |)
                      |);
                      M.read (| n |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                      "pre_dec_end",
                      []
                    |),
                    [ M.read (| self |); M.read (| advance |) ]
                  |)
                |) 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",
                        []
                      |),
                      [ BinOp.Wrap.sub (| M.read (| n |), M.read (| advance |) |) ]
                    |);
                    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 (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::double_ended::DoubleEndedIterator"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("next_back", InstanceField.Method (next_back T));
            ("nth_back", InstanceField.Method (nth_back T));
            ("advance_back_by", InstanceField.Method (advance_back_by T))
          ].
    End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_slice_iter_Iter_T.
    
    Module Impl_core_iter_traits_marker_FusedIterator_for_core_slice_iter_Iter_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_for_core_slice_iter_Iter_T.
    
    Module Impl_core_iter_traits_marker_TrustedLen_for_core_slice_iter_Iter_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::TrustedLen"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_TrustedLen_for_core_slice_iter_Iter_T.
    
    Module Impl_core_iter_traits_unchecked_iterator_UncheckedIterator_for_core_slice_iter_Iter_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ].
      
      (*
                  unsafe fn next_unchecked(&mut self) -> $elem {
                      // SAFETY: The caller promised there's at least one more item.
                      unsafe {
                          self.post_inc_start(1).$into_ref()
                      }
                  }
      *)
      Definition next_unchecked
          (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_associated_function (|
                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                "as_ref",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                      "post_inc_start",
                      []
                    |),
                    [ M.read (| self |); Value.Integer IntegerKind.Usize 1 ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::unchecked_iterator::UncheckedIterator"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("next_unchecked", InstanceField.Method (next_unchecked T)) ].
    End Impl_core_iter_traits_unchecked_iterator_UncheckedIterator_for_core_slice_iter_Iter_T.
    
    Module Impl_core_default_Default_for_core_slice_iter_Iter_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ].
      
      (*
                  fn default() -> Self {
                      (& $( $mut_ )? []).into_iter()
                  }
      *)
      Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::collect::IntoIterator",
                Ty.apply
                  (Ty.path "&")
                  []
                  [ Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 0 ] [ T ] ],
                [],
                "into_iter",
                []
              |),
              [ M.alloc (| Value.Array [] |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::default::Default"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    End Impl_core_default_Default_for_core_slice_iter_Iter_T.
    
    Module Impl_core_slice_iter_IterMut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ].
      
      (*
                  unsafe fn next_back_unchecked(&mut self) -> $elem {
                      // SAFETY: the caller promised it's not empty, so
                      // the offsetting is in-bounds and there's an element to return.
                      unsafe { self.pre_dec_end(1).$into_ref() }
                  }
      *)
      Definition next_back_unchecked
          (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_associated_function (|
                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                "as_mut",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                      "pre_dec_end",
                      []
                    |),
                    [ M.read (| self |); Value.Integer IntegerKind.Usize 1 ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_next_back_unchecked :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "next_back_unchecked" (next_back_unchecked T).
      
      (*
                  fn make_slice(&self) -> &'a [T] {
                      // SAFETY: the iterator was created from a slice with pointer
                      // `self.ptr` and length `len!(self)`. This guarantees that all
                      // the prerequisites for `from_raw_parts` are fulfilled.
                      unsafe { from_raw_parts(self.ptr.as_ptr(), len!(self)) }
                  }
      *)
      Definition make_slice (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", [ T ] |),
              [
                (* MutToConstPointer *)
                M.pointer_coercion
                  (M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::slice::iter::IterMut",
                          "ptr"
                        |)
                      |)
                    ]
                  |));
                M.read (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ len :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*mut") [] [ T ],
                                  "addr",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::slice::iter::IterMut",
                                      "end_or_len"
                                    |)
                                  |)
                                ]
                              |)
                            |) in
                          len));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ end_ :=
                            M.copy (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "*const")
                                    []
                                    [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                  "cast",
                                  [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::IterMut",
                                    "end_or_len"
                                  |)
                                ]
                              |)
                            |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                "sub_ptr",
                                []
                              |),
                              [
                                M.read (| end_ |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::IterMut",
                                    "ptr"
                                  |)
                                |)
                              ]
                            |)
                          |)))
                    ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_make_slice :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "make_slice" (make_slice T).
      
      (*
                  unsafe fn post_inc_start(&mut self, offset: usize) -> NonNull<T> {
                      let old = self.ptr;
      
                      // SAFETY: the caller guarantees that `offset` doesn't exceed `self.len()`,
                      // so this new pointer is inside `self` and thus guaranteed to be non-null.
                      unsafe {
                          if_zst!(mut self,
                              // Using the intrinsic directly avoids emitting a UbCheck
                              len => *len = crate::intrinsics::unchecked_sub( *len, offset),
                              _end => self.ptr = self.ptr.add(offset),
                          );
                      }
                      old
                  }
      *)
      Definition post_inc_start
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; offset ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let offset := M.alloc (| offset |) in
            M.read (|
              let~ old :=
                M.copy (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::slice::iter::IterMut",
                    "ptr"
                  |)
                |) in
              let~ _ :=
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ len :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "*mut")
                                    []
                                    [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                  "cast",
                                  [ Ty.path "usize" ]
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::IterMut",
                                    "end_or_len"
                                  |)
                                ]
                              |)
                            |) in
                          M.write (|
                            M.read (| len |),
                            M.call_closure (|
                              M.get_function (|
                                "core::intrinsics::unchecked_sub",
                                [ Ty.path "usize" ]
                              |),
                              [ M.read (| M.read (| len |) |); M.read (| offset |) ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ _end :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "*mut")
                                    []
                                    [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                  "cast",
                                  [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::IterMut",
                                    "end_or_len"
                                  |)
                                ]
                              |)
                            |) in
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::slice::iter::IterMut",
                              "ptr"
                            |),
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                "add",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::IterMut",
                                    "ptr"
                                  |)
                                |);
                                M.read (| offset |)
                              ]
                            |)
                          |)))
                    ]
                  |) in
                M.alloc (| Value.Tuple [] |) in
              old
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_post_inc_start :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "post_inc_start" (post_inc_start T).
      
      (*
                  unsafe fn pre_dec_end(&mut self, offset: usize) -> NonNull<T> {
                      if_zst!(mut self,
                          // SAFETY: By our precondition, `offset` can be at most the
                          // current length, so the subtraction can never overflow.
                          len => unsafe {
                              // Using the intrinsic directly avoids emitting a UbCheck
                              *len = crate::intrinsics::unchecked_sub( *len, offset);
                              self.ptr
                          },
                          // SAFETY: the caller guarantees that `offset` doesn't exceed `self.len()`,
                          // which is guaranteed to not overflow an `isize`. Also, the resulting pointer
                          // is in bounds of `slice`, which fulfills the other requirements for `offset`.
                          end => unsafe {
                              *end = end.sub(offset);
                              *end
                          },
                      )
                  }
      *)
      Definition pre_dec_end (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; offset ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let offset := M.alloc (| offset |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ len :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                              "cast",
                              [ Ty.path "usize" ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::iter::IterMut",
                                "end_or_len"
                              |)
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.write (|
                          M.read (| len |),
                          M.call_closure (|
                            M.get_function (|
                              "core::intrinsics::unchecked_sub",
                              [ Ty.path "usize" ]
                            |),
                            [ M.read (| M.read (| len |) |); M.read (| offset |) ]
                          |)
                        |) in
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::slice::iter::IterMut",
                        "ptr"
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let~ end_ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                              "cast",
                              [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::iter::IterMut",
                                "end_or_len"
                              |)
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.write (|
                          M.read (| end_ |),
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                              "sub",
                              []
                            |),
                            [ M.read (| M.read (| end_ |) |); M.read (| offset |) ]
                          |)
                        |) in
                      M.read (| end_ |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_pre_dec_end :
        forall (T : Ty.t),
        M.IsAssociatedFunction (Self T) "pre_dec_end" (pre_dec_end T).
    End Impl_core_slice_iter_IterMut_T.
    
    Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_slice_iter_IterMut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ].
      
      (*
                  fn len(&self) -> usize {
                      len!(self)
                  }
      *)
      Definition len (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ len :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "addr",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::slice::iter::IterMut",
                                  "end_or_len"
                                |)
                              |)
                            ]
                          |)
                        |) in
                      len));
                  fun γ =>
                    ltac:(M.monadic
                      (let~ end_ :=
                        M.copy (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*const") [] [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                              "cast",
                              [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::iter::IterMut",
                                "end_or_len"
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            "sub_ptr",
                            []
                          |),
                          [
                            M.read (| end_ |);
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::iter::IterMut",
                                "ptr"
                              |)
                            |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn is_empty(&self) -> bool {
                      is_empty!(self)
                  }
      *)
      Definition is_empty (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ len :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "addr",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::slice::iter::IterMut",
                                  "end_or_len"
                                |)
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (|
                        BinOp.eq (| M.read (| len |), Value.Integer IntegerKind.Usize 0 |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let~ end_ :=
                        M.copy (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*const") [] [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                              "cast",
                              [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::slice::iter::IterMut",
                                "end_or_len"
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ],
                            "eq",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::slice::iter::IterMut",
                              "ptr"
                            |);
                            end_
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::exact_size::ExactSizeIterator"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("len", InstanceField.Method (len T)); ("is_empty", InstanceField.Method (is_empty T))
          ].
    End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_slice_iter_IterMut_T.
    
    Module Impl_core_iter_traits_iterator_Iterator_for_core_slice_iter_IterMut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ].
      
      (*             type Item = $elem; *)
      Definition _Item (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
      
      (*
                  fn next(&mut self) -> Option<$elem> {
                      // could be implemented with slices, but this avoids bounds checks
      
                      // SAFETY: The call to `next_unchecked` is
                      // safe since we check if the iterator is empty first.
                      unsafe {
                          if is_empty!(self) {
                              None
                          } else {
                              Some(self.next_unchecked())
                          }
                      }
                  }
      *)
      Definition next (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.get_constant (|
                                        "core::mem::SizedTypeProperties::IS_ZST"
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ len :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "*mut") [] [ T ],
                                          "addr",
                                          []
                                        |),
                                        [
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "core::slice::iter::IterMut",
                                              "end_or_len"
                                            |)
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (|
                                    BinOp.eq (|
                                      M.read (| len |),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let~ end_ :=
                                    M.copy (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "*const")
                                            []
                                            [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                          "cast",
                                          [
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ T ]
                                          ]
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::slice::iter::IterMut",
                                            "end_or_len"
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                        [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ]
                                        ],
                                        "eq",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::IterMut",
                                          "ptr"
                                        |);
                                        end_
                                      ]
                                    |)
                                  |)))
                            ]
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::unchecked_iterator::UncheckedIterator",
                                Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                [],
                                "next_unchecked",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn size_hint(&self) -> (usize, Option<usize>) {
                      let exact = len!(self);
                      (exact, Some(exact))
                  }
      *)
      Definition size_hint (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~ exact :=
                M.copy (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ len :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*mut") [] [ T ],
                                  "addr",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::slice::iter::IterMut",
                                      "end_or_len"
                                    |)
                                  |)
                                ]
                              |)
                            |) in
                          len));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ end_ :=
                            M.copy (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "*const")
                                    []
                                    [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                  "cast",
                                  [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::IterMut",
                                    "end_or_len"
                                  |)
                                ]
                              |)
                            |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                "sub_ptr",
                                []
                              |),
                              [
                                M.read (| end_ |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::slice::iter::IterMut",
                                    "ptr"
                                  |)
                                |)
                              ]
                            |)
                          |)))
                    ]
                  |)
                |) in
              M.alloc (|
                Value.Tuple
                  [
                    M.read (| exact |);
                    Value.StructTuple "core::option::Option::Some" [ M.read (| exact |) ]
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn count(self) -> usize {
                      len!(self)
                  }
      *)
      Definition count (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ len :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*mut") [] [ T ],
                              "addr",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::slice::iter::IterMut",
                                  "end_or_len"
                                |)
                              |)
                            ]
                          |)
                        |) in
                      len));
                  fun γ =>
                    ltac:(M.monadic
                      (let~ end_ :=
                        M.copy (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "*const") [] [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                              "cast",
                              [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                self,
                                "core::slice::iter::IterMut",
                                "end_or_len"
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            "sub_ptr",
                            []
                          |),
                          [
                            M.read (| end_ |);
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                self,
                                "core::slice::iter::IterMut",
                                "ptr"
                              |)
                            |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn nth(&mut self, n: usize) -> Option<$elem> {
                      if n >= len!(self) {
                          // This iterator is now empty.
                          if_zst!(mut self,
                              len => *len = 0,
                              end => self.ptr = *end,
                          );
                          return None;
                      }
                      // SAFETY: We are in bounds. `post_inc_start` does the right thing even for ZSTs.
                      unsafe {
                          self.post_inc_start(n);
                          Some(self.next_unchecked())
                      }
                  }
      *)
      Definition nth (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ge (|
                                    M.read (| n |),
                                    M.read (|
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.get_constant (|
                                                    "core::mem::SizedTypeProperties::IS_ZST"
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              let~ len :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                                      "addr",
                                                      []
                                                    |),
                                                    [
                                                      M.read (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "core::slice::iter::IterMut",
                                                          "end_or_len"
                                                        |)
                                                      |)
                                                    ]
                                                  |)
                                                |) in
                                              len));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let~ end_ :=
                                                M.copy (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "*const")
                                                        []
                                                        [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                                      "cast",
                                                      [
                                                        Ty.apply
                                                          (Ty.path "core::ptr::non_null::NonNull")
                                                          []
                                                          [ T ]
                                                      ]
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "core::slice::iter::IterMut",
                                                        "end_or_len"
                                                      |)
                                                    ]
                                                  |)
                                                |) in
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "core::ptr::non_null::NonNull")
                                                      []
                                                      [ T ],
                                                    "sub_ptr",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| end_ |);
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "core::slice::iter::IterMut",
                                                        "ptr"
                                                      |)
                                                    |)
                                                  ]
                                                |)
                                              |)))
                                        ]
                                      |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.get_constant (|
                                                  "core::mem::SizedTypeProperties::IS_ZST"
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            let~ len :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "*mut")
                                                      []
                                                      [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                                    "cast",
                                                    [ Ty.path "usize" ]
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "core::slice::iter::IterMut",
                                                      "end_or_len"
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.write (|
                                              M.read (| len |),
                                              Value.Integer IntegerKind.Usize 0
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let~ end_ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "*mut")
                                                      []
                                                      [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                                    "cast",
                                                    [
                                                      Ty.apply
                                                        (Ty.path "core::ptr::non_null::NonNull")
                                                        []
                                                        [ T ]
                                                    ]
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "core::slice::iter::IterMut",
                                                      "end_or_len"
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.write (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "core::slice::iter::IterMut",
                                                "ptr"
                                              |),
                                              M.read (| M.read (| end_ |) |)
                                            |)))
                                      ]
                                    |) in
                                  M.return_ (| Value.StructTuple "core::option::Option::None" [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                          "post_inc_start",
                          []
                        |),
                        [ M.read (| self |); M.read (| n |) ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::unchecked_iterator::UncheckedIterator",
                            Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                            [],
                            "next_unchecked",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                      let advance = cmp::min(len!(self), n);
                      // SAFETY: By construction, `advance` does not exceed `self.len()`.
                      unsafe { self.post_inc_start(advance) };
                      NonZero::new(n - advance).map_or(Ok(()), Err)
                  }
      *)
      Definition advance_by (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ advance :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::cmp::min", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.get_constant (|
                                      "core::mem::SizedTypeProperties::IS_ZST"
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ len :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "*mut") [] [ T ],
                                        "addr",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::slice::iter::IterMut",
                                            "end_or_len"
                                          |)
                                        |)
                                      ]
                                    |)
                                  |) in
                                len));
                            fun γ =>
                              ltac:(M.monadic
                                (let~ end_ :=
                                  M.copy (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "*const")
                                          []
                                          [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                        "cast",
                                        [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ]
                                        ]
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::IterMut",
                                          "end_or_len"
                                        |)
                                      ]
                                    |)
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                      "sub_ptr",
                                      []
                                    |),
                                    [
                                      M.read (| end_ |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::IterMut",
                                          "ptr"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)))
                          ]
                        |)
                      |);
                      M.read (| n |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                      "post_inc_start",
                      []
                    |),
                    [ M.read (| self |); M.read (| advance |) ]
                  |)
                |) 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",
                        []
                      |),
                      [ BinOp.Wrap.sub (| M.read (| n |), M.read (| advance |) |) ]
                    |);
                    Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ];
                    M.constructor_as_closure "core::result::Result::Err"
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn last(mut self) -> Option<$elem> {
                      self.next_back()
                  }
      *)
      Definition last (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_trait_method (|
                "core::iter::traits::double_ended::DoubleEndedIterator",
                Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                [],
                "next_back",
                []
              |),
              [ self ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn fold<B, F>(self, init: B, mut f: F) -> B
                      where
                          F: FnMut(B, Self::Item) -> B,
                  {
                      // this implementation consists of the following optimizations compared to the
                      // default implementation:
                      // - do-while loop, as is llvm's preferred loop shape,
                      //   see https://releases.llvm.org/16.0.0/docs/LoopTerminology.html#more-canonical-loops
                      // - bumps an index instead of a pointer since the latter case inhibits
                      //   some optimizations, see #111603
                      // - avoids Option wrapping/matching
                      if is_empty!(self) {
                          return init;
                      }
                      let mut acc = init;
                      let mut i = 0;
                      let len = len!(self);
                      loop {
                          // SAFETY: the loop iterates `i in 0..len`, which always is in bounds of
                          // the slice allocation
                          acc = f(acc, unsafe { & $( $mut_ )? *self.ptr.add(i).as_ptr() });
                          // SAFETY: `i` can't overflow since it'll only reach usize::MAX if the
                          // slice had that length, in which case we'll break out of the loop
                          // after the increment
                          i = unsafe { i.unchecked_add(1) };
                          if i == len {
                              break;
                          }
                      }
                      acc
                  }
      *)
      Definition fold (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ B; F ], [ self; init; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let init := M.alloc (| init |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.get_constant (|
                                              "core::mem::SizedTypeProperties::IS_ZST"
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ len :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "addr",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    self,
                                                    "core::slice::iter::IterMut",
                                                    "end_or_len"
                                                  |)
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (|
                                          BinOp.eq (|
                                            M.read (| len |),
                                            Value.Integer IntegerKind.Usize 0
                                          |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let~ end_ :=
                                          M.copy (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "*const")
                                                  []
                                                  [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                                "cast",
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::ptr::non_null::NonNull")
                                                    []
                                                    [ T ]
                                                ]
                                              |),
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  self,
                                                  "core::slice::iter::IterMut",
                                                  "end_or_len"
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::cmp::PartialEq",
                                              Ty.apply
                                                (Ty.path "core::ptr::non_null::NonNull")
                                                []
                                                [ T ],
                                              [
                                                Ty.apply
                                                  (Ty.path "core::ptr::non_null::NonNull")
                                                  []
                                                  [ T ]
                                              ],
                                              "eq",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                self,
                                                "core::slice::iter::IterMut",
                                                "ptr"
                                              |);
                                              end_
                                            ]
                                          |)
                                        |)))
                                  ]
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| M.read (| init |) |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ acc := M.copy (| init |) in
                  let~ i := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                  let~ len :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ len :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                      "addr",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          self,
                                          "core::slice::iter::IterMut",
                                          "end_or_len"
                                        |)
                                      |)
                                    ]
                                  |)
                                |) in
                              len));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ end_ :=
                                M.copy (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "*const")
                                        []
                                        [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                      "cast",
                                      [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        self,
                                        "core::slice::iter::IterMut",
                                        "end_or_len"
                                      |)
                                    ]
                                  |)
                                |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                    "sub_ptr",
                                    []
                                  |),
                                  [
                                    M.read (| end_ |);
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        self,
                                        "core::slice::iter::IterMut",
                                        "ptr"
                                      |)
                                    |)
                                  ]
                                |)
                              |)))
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (let~ _ :=
                          M.write (|
                            acc,
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::function::FnMut",
                                F,
                                [ Ty.tuple [ B; Ty.apply (Ty.path "&mut") [] [ T ] ] ],
                                "call_mut",
                                []
                              |),
                              [
                                f;
                                Value.Tuple
                                  [
                                    M.read (| acc |);
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                        "as_ptr",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ T ],
                                            "add",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                self,
                                                "core::slice::iter::IterMut",
                                                "ptr"
                                              |)
                                            |);
                                            M.read (| i |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  ]
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.write (|
                            i,
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "usize", "unchecked_add", [] |),
                              [ M.read (| i |); Value.Integer IntegerKind.Usize 1 ]
                            |)
                          |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.eq (| M.read (| i |), M.read (| len |) |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |)))
                    |) in
                  acc
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn for_each<F>(mut self, mut f: F)
                  where
                      Self: Sized,
                      F: FnMut(Self::Item),
                  {
                      while let Some(x) = self.next() {
                          f(x);
                      }
                  }
      *)
      Definition for_each (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ F ], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              M.loop (|
                ltac:(M.monadic
                  (M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                  [],
                                  "next",
                                  []
                                |),
                                [ self ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let x := M.copy (| γ0_0 |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::function::FnMut",
                                  F,
                                  [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ T ] ] ],
                                  "call_mut",
                                  []
                                |),
                                [ f; Value.Tuple [ M.read (| x |) ] ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                                M.alloc (| Value.Tuple [] |)
                              |)
                            |)
                          |)))
                    ]
                  |)))
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn all<F>(&mut self, mut f: F) -> bool
                  where
                      Self: Sized,
                      F: FnMut(Self::Item) -> bool,
                  {
                      while let Some(x) = self.next() {
                          if !f(x) {
                              return false;
                          }
                      }
                      true
                  }
      *)
      Definition all (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ F ], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let x := M.copy (| γ0_0 |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              UnOp.not (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::function::FnMut",
                                                    F,
                                                    [
                                                      Ty.tuple
                                                        [ Ty.apply (Ty.path "&mut") [] [ T ] ]
                                                    ],
                                                    "call_mut",
                                                    []
                                                  |),
                                                  [ f; Value.Tuple [ M.read (| x |) ] ]
                                                |)
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (| M.return_ (| Value.Bool false |) |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.alloc (| Value.Bool true |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn any<F>(&mut self, mut f: F) -> bool
                  where
                      Self: Sized,
                      F: FnMut(Self::Item) -> bool,
                  {
                      while let Some(x) = self.next() {
                          if f(x) {
                              return true;
                          }
                      }
                      false
                  }
      *)
      Definition any (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ F ], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let x := M.copy (| γ0_0 |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::function::FnMut",
                                                  F,
                                                  [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ T ] ]
                                                  ],
                                                  "call_mut",
                                                  []
                                                |),
                                                [ f; Value.Tuple [ M.read (| x |) ] ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (| M.return_ (| Value.Bool true |) |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.alloc (| Value.Bool false |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn find<P>(&mut self, mut predicate: P) -> Option<Self::Item>
                  where
                      Self: Sized,
                      P: FnMut(&Self::Item) -> bool,
                  {
                      while let Some(x) = self.next() {
                          if predicate(&x) {
                              return Some(x);
                          }
                      }
                      None
                  }
      *)
      Definition find (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ P ], [ self; predicate ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let predicate := M.alloc (| predicate |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let x := M.copy (| γ0_0 |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::function::FnMut",
                                                  P,
                                                  [
                                                    Ty.tuple
                                                      [
                                                        Ty.apply
                                                          (Ty.path "&")
                                                          []
                                                          [ Ty.apply (Ty.path "&mut") [] [ T ] ]
                                                      ]
                                                  ],
                                                  "call_mut",
                                                  []
                                                |),
                                                [ predicate; Value.Tuple [ x ] ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.return_ (|
                                                Value.StructTuple
                                                  "core::option::Option::Some"
                                                  [ M.read (| x |) ]
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn find_map<B, F>(&mut self, mut f: F) -> Option<B>
                  where
                      Self: Sized,
                      F: FnMut(Self::Item) -> Option<B>,
                  {
                      while let Some(x) = self.next() {
                          if let Some(y) = f(x) {
                              return Some(y);
                          }
                      }
                      None
                  }
      *)
      Definition find_map (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ B; F ], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let x := M.copy (| γ0_0 |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::function::FnMut",
                                                F,
                                                [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ T ] ] ],
                                                "call_mut",
                                                []
                                              |),
                                              [ f; Value.Tuple [ M.read (| x |) ] ]
                                            |)
                                          |) in
                                        let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::option::Option::Some",
                                            0
                                          |) in
                                        let y := M.copy (| γ0_0 |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.return_ (|
                                                Value.StructTuple
                                                  "core::option::Option::Some"
                                                  [ M.read (| y |) ]
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn position<P>(&mut self, mut predicate: P) -> Option<usize> where
                      Self: Sized,
                      P: FnMut(Self::Item) -> bool,
                  {
                      let n = len!(self);
                      let mut i = 0;
                      while let Some(x) = self.next() {
                          if predicate(x) {
                              // SAFETY: we are guaranteed to be in bounds by the loop invariant:
                              // when `i >= n`, `self.next()` returns `None` and the loop breaks.
                              unsafe { assert_unchecked(i < n) };
                              return Some(i);
                          }
                          i += 1;
                      }
                      None
                  }
      *)
      Definition position (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ P ], [ self; predicate ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let predicate := M.alloc (| predicate |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ n :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ len :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                      "addr",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::IterMut",
                                          "end_or_len"
                                        |)
                                      |)
                                    ]
                                  |)
                                |) in
                              len));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ end_ :=
                                M.copy (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "*const")
                                        []
                                        [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                      "cast",
                                      [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "core::slice::iter::IterMut",
                                        "end_or_len"
                                      |)
                                    ]
                                  |)
                                |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                    "sub_ptr",
                                    []
                                  |),
                                  [
                                    M.read (| end_ |);
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "core::slice::iter::IterMut",
                                        "ptr"
                                      |)
                                    |)
                                  ]
                                |)
                              |)))
                        ]
                      |)
                    |) in
                  let~ i := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let x := M.copy (| γ0_0 |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::function::FnMut",
                                                    P,
                                                    [
                                                      Ty.tuple
                                                        [ Ty.apply (Ty.path "&mut") [] [ T ] ]
                                                    ],
                                                    "call_mut",
                                                    []
                                                  |),
                                                  [ predicate; Value.Tuple [ M.read (| x |) ] ]
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ _ :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::hint::assert_unchecked",
                                                        []
                                                      |),
                                                      [
                                                        BinOp.lt (|
                                                          M.read (| i |),
                                                          M.read (| n |)
                                                        |)
                                                      ]
                                                    |)
                                                  |) in
                                                M.return_ (|
                                                  Value.StructTuple
                                                    "core::option::Option::Some"
                                                    [ M.read (| i |) ]
                                                |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                let~ _ :=
                                  let β := i in
                                  M.write (|
                                    β,
                                    BinOp.Wrap.add (|
                                      M.read (| β |),
                                      Value.Integer IntegerKind.Usize 1
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn rposition<P>(&mut self, mut predicate: P) -> Option<usize> where
                      P: FnMut(Self::Item) -> bool,
                      Self: Sized + ExactSizeIterator + DoubleEndedIterator
                  {
                      let n = len!(self);
                      let mut i = n;
                      while let Some(x) = self.next_back() {
                          i -= 1;
                          if predicate(x) {
                              // SAFETY: `i` must be lower than `n` since it starts at `n`
                              // and is only decreasing.
                              unsafe { assert_unchecked(i < n) };
                              return Some(i);
                          }
                      }
                      None
                  }
      *)
      Definition rposition (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [ P ], [ self; predicate ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let predicate := M.alloc (| predicate |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ n :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ len :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                      "addr",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::IterMut",
                                          "end_or_len"
                                        |)
                                      |)
                                    ]
                                  |)
                                |) in
                              len));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ end_ :=
                                M.copy (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "*const")
                                        []
                                        [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                      "cast",
                                      [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "core::slice::iter::IterMut",
                                        "end_or_len"
                                      |)
                                    ]
                                  |)
                                |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                    "sub_ptr",
                                    []
                                  |),
                                  [
                                    M.read (| end_ |);
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "core::slice::iter::IterMut",
                                        "ptr"
                                      |)
                                    |)
                                  ]
                                |)
                              |)))
                        ]
                      |)
                    |) in
                  let~ i := M.copy (| n |) in
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::double_ended::DoubleEndedIterator",
                                        Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                        [],
                                        "next_back",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let x := M.copy (| γ0_0 |) in
                                let~ _ :=
                                  let β := i in
                                  M.write (|
                                    β,
                                    BinOp.Wrap.sub (|
                                      M.read (| β |),
                                      Value.Integer IntegerKind.Usize 1
                                    |)
                                  |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::function::FnMut",
                                                  P,
                                                  [ Ty.tuple [ Ty.associated ] ],
                                                  "call_mut",
                                                  []
                                                |),
                                                [ predicate; Value.Tuple [ M.read (| x |) ] ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              let~ _ :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::hint::assert_unchecked",
                                                      []
                                                    |),
                                                    [ BinOp.lt (| M.read (| i |), M.read (| n |) |)
                                                    ]
                                                  |)
                                                |) in
                                              M.return_ (|
                                                Value.StructTuple
                                                  "core::option::Option::Some"
                                                  [ M.read (| i |) ]
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
                      // SAFETY: the caller must guarantee that `i` is in bounds of
                      // the underlying slice, so `i` cannot overflow an `isize`, and
                      // the returned references is guaranteed to refer to an element
                      // of the slice and thus guaranteed to be valid.
                      //
                      // Also note that the caller also guarantees that we're never
                      // called with the same index again, and that no other methods
                      // that will access this subslice are called, so it is valid
                      // for the returned reference to be mutable in the case of
                      // `IterMut`
                      unsafe { & $( $mut_ )? * self.ptr.as_ptr().add(idx) }
                  }
      *)
      Definition __iterator_get_unchecked
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self 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 "*mut") [] [ T ], "add", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::slice::iter::IterMut",
                        "ptr"
                      |)
                    |)
                  ]
                |);
                M.read (| idx |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item T));
            ("next", InstanceField.Method (next T));
            ("size_hint", InstanceField.Method (size_hint T));
            ("count", InstanceField.Method (count T));
            ("nth", InstanceField.Method (nth T));
            ("advance_by", InstanceField.Method (advance_by T));
            ("last", InstanceField.Method (last T));
            ("fold", InstanceField.Method (fold T));
            ("for_each", InstanceField.Method (for_each T));
            ("all", InstanceField.Method (all T));
            ("any", InstanceField.Method (any T));
            ("find", InstanceField.Method (find T));
            ("find_map", InstanceField.Method (find_map T));
            ("position", InstanceField.Method (position T));
            ("rposition", InstanceField.Method (rposition T));
            ("__iterator_get_unchecked", InstanceField.Method (__iterator_get_unchecked T))
          ].
    End Impl_core_iter_traits_iterator_Iterator_for_core_slice_iter_IterMut_T.
    
    Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_slice_iter_IterMut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ].
      
      (*
                  fn next_back(&mut self) -> Option<$elem> {
                      // could be implemented with slices, but this avoids bounds checks
      
                      // SAFETY: The call to `next_back_unchecked`
                      // is safe since we check if the iterator is empty first.
                      unsafe {
                          if is_empty!(self) {
                              None
                          } else {
                              Some(self.next_back_unchecked())
                          }
                      }
                  }
      *)
      Definition next_back (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.get_constant (|
                                        "core::mem::SizedTypeProperties::IS_ZST"
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ len :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "*mut") [] [ T ],
                                          "addr",
                                          []
                                        |),
                                        [
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "core::slice::iter::IterMut",
                                              "end_or_len"
                                            |)
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (|
                                    BinOp.eq (|
                                      M.read (| len |),
                                      Value.Integer IntegerKind.Usize 0
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let~ end_ :=
                                    M.copy (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "*const")
                                            []
                                            [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                          "cast",
                                          [
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ T ]
                                          ]
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::slice::iter::IterMut",
                                            "end_or_len"
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                        [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ]
                                        ],
                                        "eq",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::IterMut",
                                          "ptr"
                                        |);
                                        end_
                                      ]
                                    |)
                                  |)))
                            ]
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                                "next_back_unchecked",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn nth_back(&mut self, n: usize) -> Option<$elem> {
                      if n >= len!(self) {
                          // This iterator is now empty.
                          if_zst!(mut self,
                              len => *len = 0,
                              end => *end = self.ptr,
                          );
                          return None;
                      }
                      // SAFETY: We are in bounds. `pre_dec_end` does the right thing even for ZSTs.
                      unsafe {
                          self.pre_dec_end(n);
                          Some(self.next_back_unchecked())
                      }
                  }
      *)
      Definition nth_back (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ge (|
                                    M.read (| n |),
                                    M.read (|
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.get_constant (|
                                                    "core::mem::SizedTypeProperties::IS_ZST"
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              let~ len :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply (Ty.path "*mut") [] [ T ],
                                                      "addr",
                                                      []
                                                    |),
                                                    [
                                                      M.read (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "core::slice::iter::IterMut",
                                                          "end_or_len"
                                                        |)
                                                      |)
                                                    ]
                                                  |)
                                                |) in
                                              len));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let~ end_ :=
                                                M.copy (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "*const")
                                                        []
                                                        [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                                      "cast",
                                                      [
                                                        Ty.apply
                                                          (Ty.path "core::ptr::non_null::NonNull")
                                                          []
                                                          [ T ]
                                                      ]
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "core::slice::iter::IterMut",
                                                        "end_or_len"
                                                      |)
                                                    ]
                                                  |)
                                                |) in
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "core::ptr::non_null::NonNull")
                                                      []
                                                      [ T ],
                                                    "sub_ptr",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| end_ |);
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "core::slice::iter::IterMut",
                                                        "ptr"
                                                      |)
                                                    |)
                                                  ]
                                                |)
                                              |)))
                                        ]
                                      |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.get_constant (|
                                                  "core::mem::SizedTypeProperties::IS_ZST"
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            let~ len :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "*mut")
                                                      []
                                                      [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                                    "cast",
                                                    [ Ty.path "usize" ]
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "core::slice::iter::IterMut",
                                                      "end_or_len"
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.write (|
                                              M.read (| len |),
                                              Value.Integer IntegerKind.Usize 0
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let~ end_ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "*mut")
                                                      []
                                                      [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                                    "cast",
                                                    [
                                                      Ty.apply
                                                        (Ty.path "core::ptr::non_null::NonNull")
                                                        []
                                                        [ T ]
                                                    ]
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "core::slice::iter::IterMut",
                                                      "end_or_len"
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            M.write (|
                                              M.read (| end_ |),
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "core::slice::iter::IterMut",
                                                  "ptr"
                                                |)
                                              |)
                                            |)))
                                      ]
                                    |) in
                                  M.return_ (| Value.StructTuple "core::option::Option::None" [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                          "pre_dec_end",
                          []
                        |),
                        [ M.read (| self |); M.read (| n |) ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                            "next_back_unchecked",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                      let advance = cmp::min(len!(self), n);
                      // SAFETY: By construction, `advance` does not exceed `self.len()`.
                      unsafe { self.pre_dec_end(advance) };
                      NonZero::new(n - advance).map_or(Ok(()), Err)
                  }
      *)
      Definition advance_back_by
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ advance :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::cmp::min", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.get_constant (|
                                      "core::mem::SizedTypeProperties::IS_ZST"
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ len :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "*mut") [] [ T ],
                                        "addr",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::slice::iter::IterMut",
                                            "end_or_len"
                                          |)
                                        |)
                                      ]
                                    |)
                                  |) in
                                len));
                            fun γ =>
                              ltac:(M.monadic
                                (let~ end_ :=
                                  M.copy (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "*const")
                                          []
                                          [ Ty.apply (Ty.path "*mut") [] [ T ] ],
                                        "cast",
                                        [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ]
                                        ]
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::IterMut",
                                          "end_or_len"
                                        |)
                                      ]
                                    |)
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                      "sub_ptr",
                                      []
                                    |),
                                    [
                                      M.read (| end_ |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::slice::iter::IterMut",
                                          "ptr"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)))
                          ]
                        |)
                      |);
                      M.read (| n |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                      "pre_dec_end",
                      []
                    |),
                    [ M.read (| self |); M.read (| advance |) ]
                  |)
                |) 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",
                        []
                      |),
                      [ BinOp.Wrap.sub (| M.read (| n |), M.read (| advance |) |) ]
                    |);
                    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 (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::double_ended::DoubleEndedIterator"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("next_back", InstanceField.Method (next_back T));
            ("nth_back", InstanceField.Method (nth_back T));
            ("advance_back_by", InstanceField.Method (advance_back_by T))
          ].
    End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_slice_iter_IterMut_T.
    
    Module Impl_core_iter_traits_marker_FusedIterator_for_core_slice_iter_IterMut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_for_core_slice_iter_IterMut_T.
    
    Module Impl_core_iter_traits_marker_TrustedLen_for_core_slice_iter_IterMut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::TrustedLen"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_TrustedLen_for_core_slice_iter_IterMut_T.
    
    Module Impl_core_iter_traits_unchecked_iterator_UncheckedIterator_for_core_slice_iter_IterMut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ].
      
      (*
                  unsafe fn next_unchecked(&mut self) -> $elem {
                      // SAFETY: The caller promised there's at least one more item.
                      unsafe {
                          self.post_inc_start(1).$into_ref()
                      }
                  }
      *)
      Definition next_unchecked
          (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_associated_function (|
                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                "as_mut",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ],
                      "post_inc_start",
                      []
                    |),
                    [ M.read (| self |); Value.Integer IntegerKind.Usize 1 ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::unchecked_iterator::UncheckedIterator"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("next_unchecked", InstanceField.Method (next_unchecked T)) ].
    End Impl_core_iter_traits_unchecked_iterator_UncheckedIterator_for_core_slice_iter_IterMut_T.
    
    Module Impl_core_default_Default_for_core_slice_iter_IterMut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ].
      
      (*
                  fn default() -> Self {
                      (& $( $mut_ )? []).into_iter()
                  }
      *)
      Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::collect::IntoIterator",
                Ty.apply
                  (Ty.path "&mut")
                  []
                  [ Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 0 ] [ T ] ],
                [],
                "into_iter",
                []
              |),
              [ M.alloc (| Value.Array [] |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::default::Default"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    End Impl_core_default_Default_for_core_slice_iter_IterMut_T.
    
    Module Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_SplitN_T_P.
      Definition Self (T P : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::slice::iter::SplitN") [] [ T; P ].
      
      (*             type Item = $iter_of; *)
      Definition _Item (T P : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
                  fn next(&mut self) -> Option<$iter_of> {
                      self.inner.next()
                  }
      *)
      Definition next (T P : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T P in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::slice::iter::GenericSplitN")
                  []
                  [ Ty.apply (Ty.path "core::slice::iter::Split") [] [ T; P ] ],
                [],
                "next",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::slice::iter::SplitN",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn size_hint(&self) -> (usize, Option<usize>) {
                      self.inner.size_hint()
                  }
      *)
      Definition size_hint (T P : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T P in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::slice::iter::GenericSplitN")
                  []
                  [ Ty.apply (Ty.path "core::slice::iter::Split") [] [ T; P ] ],
                [],
                "size_hint",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::slice::iter::SplitN",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T P : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          (Self T P)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item T P));
            ("next", InstanceField.Method (next T P));
            ("size_hint", InstanceField.Method (size_hint T P))
          ].
    End Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_SplitN_T_P.
    
    Module Impl_core_iter_traits_marker_FusedIterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_SplitN_T_P.
      Definition Self (T P : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::slice::iter::SplitN") [] [ T; P ].
      
      Axiom Implements :
        forall (T P : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          (Self T P)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_SplitN_T_P.
    
    Module Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_RSplitN_T_P.
      Definition Self (T P : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::slice::iter::RSplitN") [] [ T; P ].
      
      (*             type Item = $iter_of; *)
      Definition _Item (T P : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
                  fn next(&mut self) -> Option<$iter_of> {
                      self.inner.next()
                  }
      *)
      Definition next (T P : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T P in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::slice::iter::GenericSplitN")
                  []
                  [ Ty.apply (Ty.path "core::slice::iter::RSplit") [] [ T; P ] ],
                [],
                "next",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::slice::iter::RSplitN",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn size_hint(&self) -> (usize, Option<usize>) {
                      self.inner.size_hint()
                  }
      *)
      Definition size_hint (T P : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T P in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::slice::iter::GenericSplitN")
                  []
                  [ Ty.apply (Ty.path "core::slice::iter::RSplit") [] [ T; P ] ],
                [],
                "size_hint",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::slice::iter::RSplitN",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T P : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          (Self T P)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item T P));
            ("next", InstanceField.Method (next T P));
            ("size_hint", InstanceField.Method (size_hint T P))
          ].
    End Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_RSplitN_T_P.
    
    Module Impl_core_iter_traits_marker_FusedIterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_RSplitN_T_P.
      Definition Self (T P : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::slice::iter::RSplitN") [] [ T; P ].
      
      Axiom Implements :
        forall (T P : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          (Self T P)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_RSplitN_T_P.
    
    Module Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_SplitNMut_T_P.
      Definition Self (T P : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::slice::iter::SplitNMut") [] [ T; P ].
      
      (*             type Item = $iter_of; *)
      Definition _Item (T P : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
                  fn next(&mut self) -> Option<$iter_of> {
                      self.inner.next()
                  }
      *)
      Definition next (T P : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T P in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::slice::iter::GenericSplitN")
                  []
                  [ Ty.apply (Ty.path "core::slice::iter::SplitMut") [] [ T; P ] ],
                [],
                "next",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::slice::iter::SplitNMut",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn size_hint(&self) -> (usize, Option<usize>) {
                      self.inner.size_hint()
                  }
      *)
      Definition size_hint (T P : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T P in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::slice::iter::GenericSplitN")
                  []
                  [ Ty.apply (Ty.path "core::slice::iter::SplitMut") [] [ T; P ] ],
                [],
                "size_hint",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::slice::iter::SplitNMut",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T P : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          (Self T P)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item T P));
            ("next", InstanceField.Method (next T P));
            ("size_hint", InstanceField.Method (size_hint T P))
          ].
    End Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_SplitNMut_T_P.
    
    Module Impl_core_iter_traits_marker_FusedIterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_SplitNMut_T_P.
      Definition Self (T P : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::slice::iter::SplitNMut") [] [ T; P ].
      
      Axiom Implements :
        forall (T P : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          (Self T P)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_SplitNMut_T_P.
    
    Module Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_RSplitNMut_T_P.
      Definition Self (T P : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::slice::iter::RSplitNMut") [] [ T; P ].
      
      (*             type Item = $iter_of; *)
      Definition _Item (T P : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
                  fn next(&mut self) -> Option<$iter_of> {
                      self.inner.next()
                  }
      *)
      Definition next (T P : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T P in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::slice::iter::GenericSplitN")
                  []
                  [ Ty.apply (Ty.path "core::slice::iter::RSplitMut") [] [ T; P ] ],
                [],
                "next",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::slice::iter::RSplitNMut",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
                  fn size_hint(&self) -> (usize, Option<usize>) {
                      self.inner.size_hint()
                  }
      *)
      Definition size_hint (T P : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T P in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply
                  (Ty.path "core::slice::iter::GenericSplitN")
                  []
                  [ Ty.apply (Ty.path "core::slice::iter::RSplitMut") [] [ T; P ] ],
                [],
                "size_hint",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::slice::iter::RSplitNMut",
                  "inner"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T P : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          (Self T P)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item T P));
            ("next", InstanceField.Method (next T P));
            ("size_hint", InstanceField.Method (size_hint T P))
          ].
    End Impl_core_iter_traits_iterator_Iterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_RSplitNMut_T_P.
    
    Module Impl_core_iter_traits_marker_FusedIterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_RSplitNMut_T_P.
      Definition Self (T P : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::slice::iter::RSplitNMut") [] [ T; P ].
      
      Axiom Implements :
        forall (T P : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          (Self T P)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_where_core_ops_function_FnMut_P_Tuple_ref__T__for_core_slice_iter_RSplitNMut_T_P.
  End iter.
End slice.
