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

Module collections.
  Module vec_deque.
    Module into_iter.
      (* StructRecord
        {
          name := "IntoIter";
          const_params := [];
          ty_params := [ "T"; "A" ];
          fields :=
            [ ("inner", Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ]) ];
        } *)
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_T_where_core_clone_Clone_A_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::into_iter::IntoIter") [] [ T; A ].
        
        (* Clone *)
        Definition clone (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructRecord
                "alloc::collections::vec_deque::into_iter::IntoIter"
                [
                  ("inner",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::collections::vec_deque::into_iter::IntoIter",
                          "inner"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::clone::Clone"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method (clone T A)) ].
      End Impl_core_clone_Clone_where_core_clone_Clone_T_where_core_clone_Clone_A_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
      
      Module Impl_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::into_iter::IntoIter") [] [ T; A ].
        
        (*
            pub(super) fn new(inner: VecDeque<T, A>) -> Self {
                IntoIter { inner }
            }
        *)
        Definition new (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ inner ] =>
            ltac:(M.monadic
              (let inner := M.alloc (| inner |) in
              Value.StructRecord
                "alloc::collections::vec_deque::into_iter::IntoIter"
                [ ("inner", M.read (| inner |)) ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (T A : Ty.t),
          M.IsAssociatedFunction (Self T A) "new" (new T A).
        
        (*
            pub(super) fn into_vecdeque(self) -> VecDeque<T, A> {
                self.inner
            }
        *)
        Definition into_vecdeque
            (T A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  self,
                  "alloc::collections::vec_deque::into_iter::IntoIter",
                  "inner"
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_into_vecdeque :
          forall (T A : Ty.t),
          M.IsAssociatedFunction (Self T A) "into_vecdeque" (into_vecdeque T A).
      End Impl_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::into_iter::IntoIter") [] [ T; A ].
        
        (*
            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                f.debug_tuple("IntoIter").field(&self.inner).finish()
            }
        *)
        Definition fmt (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::builders::DebugTuple",
                  "finish",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::builders::DebugTuple",
                      "field",
                      []
                    |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "debug_tuple",
                            []
                          |),
                          [ M.read (| f |); M.read (| Value.String "IntoIter" |) ]
                        |)
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "alloc::collections::vec_deque::into_iter::IntoIter",
                        "inner"
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::fmt::Debug"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method (fmt T A)) ].
      End Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::into_iter::IntoIter") [] [ T; A ].
        
        (*     type Item = T; *)
        Definition _Item (T A : Ty.t) : Ty.t := T.
        
        (*
            fn next(&mut self) -> Option<T> {
                self.inner.pop_front()
            }
        *)
        Definition next (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                  "pop_front",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "alloc::collections::vec_deque::into_iter::IntoIter",
                    "inner"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                let len = self.inner.len();
                (len, Some(len))
            }
        *)
        Definition size_hint
            (T A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                        "len",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::collections::vec_deque::into_iter::IntoIter",
                          "inner"
                        |)
                      ]
                    |)
                  |) in
                M.alloc (|
                  Value.Tuple
                    [
                      M.read (| len |);
                      Value.StructTuple "core::option::Option::Some" [ M.read (| len |) ]
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                let len = self.inner.len;
                let rem = if len < n {
                    self.inner.clear();
                    n - len
                } else {
                    self.inner.drain(..n);
                    0
                };
                NonZero::new(rem).map_or(Ok(()), Err)
            }
        *)
        Definition advance_by
            (T A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.read (|
                let~ len :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "alloc::collections::vec_deque::into_iter::IntoIter",
                        "inner"
                      |),
                      "alloc::collections::vec_deque::VecDeque",
                      "len"
                    |)
                  |) in
                let~ rem :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (| BinOp.lt (| M.read (| len |), M.read (| n |) |) |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::vec_deque::VecDeque")
                                      []
                                      [ T; A ],
                                    "clear",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "alloc::collections::vec_deque::into_iter::IntoIter",
                                      "inner"
                                    |)
                                  ]
                                |)
                              |) in
                            M.alloc (| BinOp.Wrap.sub (| M.read (| n |), M.read (| len |) |) |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::vec_deque::VecDeque")
                                      []
                                      [ T; A ],
                                    "drain",
                                    [
                                      Ty.apply
                                        (Ty.path "core::ops::range::RangeTo")
                                        []
                                        [ Ty.path "usize" ]
                                    ]
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "alloc::collections::vec_deque::into_iter::IntoIter",
                                      "inner"
                                    |);
                                    Value.StructRecord
                                      "core::ops::range::RangeTo"
                                      [ ("end_", M.read (| n |)) ]
                                  ]
                                |)
                              |) in
                            M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ],
                      "map_or",
                      [
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [
                            Ty.tuple [];
                            Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                          ];
                        Ty.function
                          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                          ]
                          (Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [
                              Ty.tuple [];
                              Ty.apply
                                (Ty.path "core::num::nonzero::NonZero")
                                []
                                [ Ty.path "usize" ]
                            ])
                      ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                          "new",
                          []
                        |),
                        [ M.read (| rem |) ]
                      |);
                      Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ];
                      M.constructor_as_closure "core::result::Result::Err"
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn count(self) -> usize {
                self.inner.len
            }
        *)
        Definition count (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "alloc::collections::vec_deque::into_iter::IntoIter",
                    "inner"
                  |),
                  "alloc::collections::vec_deque::VecDeque",
                  "len"
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_fold<B, F, R>(&mut self, mut init: B, mut f: F) -> R
            where
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                struct Guard<'a, T, A: Allocator> {
                    deque: &'a mut VecDeque<T, A>,
                    // `consumed <= deque.len` always holds.
                    consumed: usize,
                }
        
                impl<'a, T, A: Allocator> Drop for Guard<'a, T, A> {
                    fn drop(&mut self) {
                        self.deque.len -= self.consumed;
                        self.deque.head = self.deque.to_physical_idx(self.consumed);
                    }
                }
        
                let mut guard = Guard { deque: &mut self.inner, consumed: 0 };
        
                let (head, tail) = guard.deque.as_slices();
        
                init = head
                    .iter()
                    .map(|elem| {
                        guard.consumed += 1;
                        // SAFETY: Because we incremented `guard.consumed`, the
                        // deque effectively forgot the element, so we can take
                        // ownership
                        unsafe { ptr::read(elem) }
                    })
                    .try_fold(init, &mut f)?;
        
                tail.iter()
                    .map(|elem| {
                        guard.consumed += 1;
                        // SAFETY: Same as above.
                        unsafe { ptr::read(elem) }
                    })
                    .try_fold(init, &mut f)
            }
        *)
        Definition try_fold
            (T A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [ B; F; R ], [ 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~ guard :=
                      M.alloc (|
                        Value.StructRecord
                          "alloc::collections::vec_deque::into_iter::try_fold::Guard"
                          [
                            ("deque",
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::vec_deque::into_iter::IntoIter",
                                "inner"
                              |));
                            ("consumed", Value.Integer IntegerKind.Usize 0)
                          ]
                      |) in
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::vec_deque::VecDeque")
                              []
                              [ T; A ],
                            "as_slices",
                            []
                          |),
                          [
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                guard,
                                "alloc::collections::vec_deque::into_iter::try_fold::Guard",
                                "deque"
                              |)
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let head := M.copy (| γ0_0 |) in
                            let tail := M.copy (| γ0_1 |) in
                            let~ _ :=
                              M.write (|
                                init,
                                M.read (|
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::try_trait::Try",
                                          R,
                                          [],
                                          "branch",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::iterator::Iterator",
                                              Ty.apply
                                                (Ty.path "core::iter::adapters::map::Map")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::slice::iter::Iter")
                                                    []
                                                    [ T ];
                                                  Ty.function
                                                    [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ]
                                                    T
                                                ],
                                              [],
                                              "try_fold",
                                              [ B; Ty.apply (Ty.path "&mut") [] [ F ]; R ]
                                            |),
                                            [
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::iter::traits::iterator::Iterator",
                                                    Ty.apply
                                                      (Ty.path "core::slice::iter::Iter")
                                                      []
                                                      [ T ],
                                                    [],
                                                    "map",
                                                    [
                                                      T;
                                                      Ty.function
                                                        [
                                                          Ty.tuple
                                                            [ Ty.apply (Ty.path "&") [] [ T ] ]
                                                        ]
                                                        T
                                                    ]
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply (Ty.path "slice") [] [ T ],
                                                        "iter",
                                                        []
                                                      |),
                                                      [ M.read (| head |) ]
                                                    |);
                                                    M.closure
                                                      (fun γ =>
                                                        ltac:(M.monadic
                                                          match γ with
                                                          | [ α0 ] =>
                                                            ltac:(M.monadic
                                                              (M.match_operator (|
                                                                M.alloc (| α0 |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let elem := M.copy (| γ |) in
                                                                      M.read (|
                                                                        let~ _ :=
                                                                          let β :=
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              guard,
                                                                              "alloc::collections::vec_deque::into_iter::try_fold::Guard",
                                                                              "consumed"
                                                                            |) in
                                                                          M.write (|
                                                                            β,
                                                                            BinOp.Wrap.add (|
                                                                              M.read (| β |),
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                1
                                                                            |)
                                                                          |) in
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_function (|
                                                                              "core::ptr::read",
                                                                              [ T ]
                                                                            |),
                                                                            [ M.read (| elem |) ]
                                                                          |)
                                                                        |)
                                                                      |)))
                                                                ]
                                                              |)))
                                                          | _ =>
                                                            M.impossible "wrong number of arguments"
                                                          end))
                                                  ]
                                                |)
                                              |);
                                              M.read (| init |);
                                              f
                                            ]
                                          |)
                                        ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::ops::control_flow::ControlFlow::Break",
                                              0
                                            |) in
                                          let residual := M.copy (| γ0_0 |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                M.return_ (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::FromResidual",
                                                      R,
                                                      [ Ty.associated ],
                                                      "from_residual",
                                                      []
                                                    |),
                                                    [ M.read (| residual |) ]
                                                  |)
                                                |)
                                              |)
                                            |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::ops::control_flow::ControlFlow::Continue",
                                              0
                                            |) in
                                          let val := M.copy (| γ0_0 |) in
                                          val))
                                    ]
                                  |)
                                |)
                              |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "core::iter::adapters::map::Map")
                                    []
                                    [
                                      Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ];
                                      Ty.function [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ] T
                                    ],
                                  [],
                                  "try_fold",
                                  [ B; Ty.apply (Ty.path "&mut") [] [ F ]; R ]
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                        [],
                                        "map",
                                        [
                                          T;
                                          Ty.function
                                            [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ]
                                            T
                                        ]
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "slice") [] [ T ],
                                            "iter",
                                            []
                                          |),
                                          [ M.read (| tail |) ]
                                        |);
                                        M.closure
                                          (fun γ =>
                                            ltac:(M.monadic
                                              match γ with
                                              | [ α0 ] =>
                                                ltac:(M.monadic
                                                  (M.match_operator (|
                                                    M.alloc (| α0 |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let elem := M.copy (| γ |) in
                                                          M.read (|
                                                            let~ _ :=
                                                              let β :=
                                                                M.SubPointer.get_struct_record_field (|
                                                                  guard,
                                                                  "alloc::collections::vec_deque::into_iter::try_fold::Guard",
                                                                  "consumed"
                                                                |) in
                                                              M.write (|
                                                                β,
                                                                BinOp.Wrap.add (|
                                                                  M.read (| β |),
                                                                  Value.Integer IntegerKind.Usize 1
                                                                |)
                                                              |) in
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::ptr::read",
                                                                  [ T ]
                                                                |),
                                                                [ M.read (| elem |) ]
                                                              |)
                                                            |)
                                                          |)))
                                                    ]
                                                  |)))
                                              | _ => M.impossible "wrong number of arguments"
                                              end))
                                      ]
                                    |)
                                  |);
                                  M.read (| init |);
                                  f
                                ]
                              |)
                            |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn fold<B, F>(mut self, init: B, mut f: F) -> B
            where
                F: FnMut(B, Self::Item) -> B,
            {
                match self.try_fold(init, |b, item| Ok::<B, !>(f(b, item))) {
                    Ok(b) => b,
                }
            }
        *)
        Definition fold (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T A 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.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply
                          (Ty.path "alloc::collections::vec_deque::into_iter::IntoIter")
                          []
                          [ T; A ],
                        [],
                        "try_fold",
                        [
                          B;
                          Ty.function
                            [ Ty.tuple [ B; T ] ]
                            (Ty.apply (Ty.path "core::result::Result") [] [ B; Ty.path "never" ]);
                          Ty.apply (Ty.path "core::result::Result") [] [ B; Ty.path "never" ]
                        ]
                      |),
                      [
                        self;
                        M.read (| init |);
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [ α0; α1 ] =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let b := M.copy (| γ |) in
                                          M.match_operator (|
                                            M.alloc (| α1 |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let item := M.copy (| γ |) in
                                                  Value.StructTuple
                                                    "core::result::Result::Ok"
                                                    [
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::function::FnMut",
                                                          F,
                                                          [ Ty.tuple [ B; T ] ],
                                                          "call_mut",
                                                          []
                                                        |),
                                                        [
                                                          f;
                                                          Value.Tuple
                                                            [ M.read (| b |); M.read (| item |) ]
                                                        ]
                                                      |)
                                                    ]))
                                            ]
                                          |)))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::result::Result::Ok",
                            0
                          |) in
                        let b := M.copy (| γ0_0 |) in
                        b))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn last(mut self) -> Option<Self::Item> {
                self.inner.pop_back()
            }
        *)
        Definition last (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                  "pop_back",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "alloc::collections::vec_deque::into_iter::IntoIter",
                    "inner"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn next_chunk<const N: usize>(
                &mut self,
            ) -> Result<[Self::Item; N], array::IntoIter<Self::Item, N>> {
                let mut raw_arr = [const { MaybeUninit::uninit() }; N];
                let raw_arr_ptr = raw_arr.as_mut_ptr().cast();
                let (head, tail) = self.inner.as_slices();
        
                if head.len() >= N {
                    // SAFETY: By manually adjusting the head and length of the deque, we effectively
                    // make it forget the first `N` elements, so taking ownership of them is safe.
                    unsafe { ptr::copy_nonoverlapping(head.as_ptr(), raw_arr_ptr, N) };
                    self.inner.head = self.inner.to_physical_idx(N);
                    self.inner.len -= N;
                    // SAFETY: We initialized the entire array with items from `head`
                    return Ok(unsafe { raw_arr.transpose().assume_init() });
                }
        
                // SAFETY: Same argument as above.
                unsafe { ptr::copy_nonoverlapping(head.as_ptr(), raw_arr_ptr, head.len()) };
                let remaining = N - head.len();
        
                if tail.len() >= remaining {
                    // SAFETY: Same argument as above.
                    unsafe {
                        ptr::copy_nonoverlapping(tail.as_ptr(), raw_arr_ptr.add(head.len()), remaining)
                    };
                    self.inner.head = self.inner.to_physical_idx(N);
                    self.inner.len -= N;
                    // SAFETY: We initialized the entire array with items from `head` and `tail`
                    Ok(unsafe { raw_arr.transpose().assume_init() })
                } else {
                    // SAFETY: Same argument as above.
                    unsafe {
                        ptr::copy_nonoverlapping(tail.as_ptr(), raw_arr_ptr.add(head.len()), tail.len())
                    };
                    let init = head.len() + tail.len();
                    // We completely drained all the deques elements.
                    self.inner.head = 0;
                    self.inner.len = 0;
                    // SAFETY: We copied all elements from both slices to the beginning of the array, so
                    // the given range is initialized.
                    Err(unsafe { array::IntoIter::new_unchecked(raw_arr, 0..init) })
                }
            }
        *)
        Definition next_chunk
            (T A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [ N ], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ raw_arr :=
                      M.alloc (|
                        repeat (|
                          M.read (|
                            M.get_constant (|
                              "alloc::collections::vec_deque::into_iter::next_chunk_discriminant"
                            |)
                          |),
                          N
                        |)
                      |) in
                    let~ raw_arr_ptr :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "*mut")
                              []
                              [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                              ],
                            "cast",
                            [ T ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                      []
                                      [ T ]
                                  ],
                                "as_mut_ptr",
                                []
                              |),
                              [ raw_arr ]
                            |)
                          ]
                        |)
                      |) in
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::vec_deque::VecDeque")
                              []
                              [ T; A ],
                            "as_slices",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "alloc::collections::vec_deque::into_iter::IntoIter",
                              "inner"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let head := M.copy (| γ0_0 |) in
                            let tail := M.copy (| γ0_1 |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            BinOp.ge (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply (Ty.path "slice") [] [ T ],
                                                  "len",
                                                  []
                                                |),
                                                [ M.read (| head |) ]
                                              |),
                                              M.read (|
                                                M.get_constant (|
                                                  "alloc::collections::vec_deque::into_iter::next_chunk::N"
                                                |)
                                              |)
                                            |)
                                          |)) 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::intrinsics::copy_nonoverlapping",
                                                    [ T ]
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply (Ty.path "slice") [] [ T ],
                                                        "as_ptr",
                                                        []
                                                      |),
                                                      [ M.read (| head |) ]
                                                    |);
                                                    M.read (| raw_arr_ptr |);
                                                    M.read (|
                                                      M.get_constant (|
                                                        "alloc::collections::vec_deque::into_iter::next_chunk::N"
                                                      |)
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "alloc::collections::vec_deque::into_iter::IntoIter",
                                                    "inner"
                                                  |),
                                                  "alloc::collections::vec_deque::VecDeque",
                                                  "head"
                                                |),
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path
                                                        "alloc::collections::vec_deque::VecDeque")
                                                      []
                                                      [ T; A ],
                                                    "to_physical_idx",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "alloc::collections::vec_deque::into_iter::IntoIter",
                                                      "inner"
                                                    |);
                                                    M.read (|
                                                      M.get_constant (|
                                                        "alloc::collections::vec_deque::into_iter::next_chunk::N"
                                                      |)
                                                    |)
                                                  ]
                                                |)
                                              |) in
                                            let~ _ :=
                                              let β :=
                                                M.SubPointer.get_struct_record_field (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "alloc::collections::vec_deque::into_iter::IntoIter",
                                                    "inner"
                                                  |),
                                                  "alloc::collections::vec_deque::VecDeque",
                                                  "len"
                                                |) in
                                              M.write (|
                                                β,
                                                BinOp.Wrap.sub (|
                                                  M.read (| β |),
                                                  M.read (|
                                                    M.get_constant (|
                                                      "alloc::collections::vec_deque::into_iter::next_chunk::N"
                                                    |)
                                                  |)
                                                |)
                                              |) in
                                            M.return_ (|
                                              Value.StructTuple
                                                "core::result::Result::Ok"
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path
                                                          "core::mem::maybe_uninit::MaybeUninit")
                                                        []
                                                        [ Ty.apply (Ty.path "array") [ N ] [ T ] ],
                                                      "assume_init",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "array")
                                                            [ N ]
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "core::mem::maybe_uninit::MaybeUninit")
                                                                []
                                                                [ T ]
                                                            ],
                                                          "transpose",
                                                          []
                                                        |),
                                                        [ M.read (| raw_arr |) ]
                                                      |)
                                                    ]
                                                  |)
                                                ]
                                            |)
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_function (|
                                    "core::intrinsics::copy_nonoverlapping",
                                    [ T ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ T ],
                                        "as_ptr",
                                        []
                                      |),
                                      [ M.read (| head |) ]
                                    |);
                                    M.read (| raw_arr_ptr |);
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ T ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| head |) ]
                                    |)
                                  ]
                                |)
                              |) in
                            let~ remaining :=
                              M.alloc (|
                                BinOp.Wrap.sub (|
                                  M.read (|
                                    M.get_constant (|
                                      "alloc::collections::vec_deque::into_iter::next_chunk::N"
                                    |)
                                  |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| head |) ]
                                  |)
                                |)
                              |) in
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.ge (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "slice") [] [ T ],
                                                "len",
                                                []
                                              |),
                                              [ M.read (| tail |) ]
                                            |),
                                            M.read (| remaining |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_function (|
                                            "core::intrinsics::copy_nonoverlapping",
                                            [ T ]
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "slice") [] [ T ],
                                                "as_ptr",
                                                []
                                              |),
                                              [ M.read (| tail |) ]
                                            |);
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "add",
                                                []
                                              |),
                                              [
                                                M.read (| raw_arr_ptr |);
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "slice") [] [ T ],
                                                    "len",
                                                    []
                                                  |),
                                                  [ M.read (| head |) ]
                                                |)
                                              ]
                                            |);
                                            M.read (| remaining |)
                                          ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "alloc::collections::vec_deque::into_iter::IntoIter",
                                            "inner"
                                          |),
                                          "alloc::collections::vec_deque::VecDeque",
                                          "head"
                                        |),
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "alloc::collections::vec_deque::VecDeque")
                                              []
                                              [ T; A ],
                                            "to_physical_idx",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "alloc::collections::vec_deque::into_iter::IntoIter",
                                              "inner"
                                            |);
                                            M.read (|
                                              M.get_constant (|
                                                "alloc::collections::vec_deque::into_iter::next_chunk::N"
                                              |)
                                            |)
                                          ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      let β :=
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "alloc::collections::vec_deque::into_iter::IntoIter",
                                            "inner"
                                          |),
                                          "alloc::collections::vec_deque::VecDeque",
                                          "len"
                                        |) in
                                      M.write (|
                                        β,
                                        BinOp.Wrap.sub (|
                                          M.read (| β |),
                                          M.read (|
                                            M.get_constant (|
                                              "alloc::collections::vec_deque::into_iter::next_chunk::N"
                                            |)
                                          |)
                                        |)
                                      |) in
                                    M.alloc (|
                                      Value.StructTuple
                                        "core::result::Result::Ok"
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                                []
                                                [ Ty.apply (Ty.path "array") [ N ] [ T ] ],
                                              "assume_init",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "array")
                                                    [ N ]
                                                    [
                                                      Ty.apply
                                                        (Ty.path
                                                          "core::mem::maybe_uninit::MaybeUninit")
                                                        []
                                                        [ T ]
                                                    ],
                                                  "transpose",
                                                  []
                                                |),
                                                [ M.read (| raw_arr |) ]
                                              |)
                                            ]
                                          |)
                                        ]
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_function (|
                                            "core::intrinsics::copy_nonoverlapping",
                                            [ T ]
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "slice") [] [ T ],
                                                "as_ptr",
                                                []
                                              |),
                                              [ M.read (| tail |) ]
                                            |);
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*mut") [] [ T ],
                                                "add",
                                                []
                                              |),
                                              [
                                                M.read (| raw_arr_ptr |);
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "slice") [] [ T ],
                                                    "len",
                                                    []
                                                  |),
                                                  [ M.read (| head |) ]
                                                |)
                                              ]
                                            |);
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "slice") [] [ T ],
                                                "len",
                                                []
                                              |),
                                              [ M.read (| tail |) ]
                                            |)
                                          ]
                                        |)
                                      |) in
                                    let~ init :=
                                      M.alloc (|
                                        BinOp.Wrap.add (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply (Ty.path "slice") [] [ T ],
                                              "len",
                                              []
                                            |),
                                            [ M.read (| head |) ]
                                          |),
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply (Ty.path "slice") [] [ T ],
                                              "len",
                                              []
                                            |),
                                            [ M.read (| tail |) ]
                                          |)
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "alloc::collections::vec_deque::into_iter::IntoIter",
                                            "inner"
                                          |),
                                          "alloc::collections::vec_deque::VecDeque",
                                          "head"
                                        |),
                                        Value.Integer IntegerKind.Usize 0
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "alloc::collections::vec_deque::into_iter::IntoIter",
                                            "inner"
                                          |),
                                          "alloc::collections::vec_deque::VecDeque",
                                          "len"
                                        |),
                                        Value.Integer IntegerKind.Usize 0
                                      |) in
                                    M.alloc (|
                                      Value.StructTuple
                                        "core::result::Result::Err"
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "core::array::iter::IntoIter")
                                                [ N ]
                                                [ T ],
                                              "new_unchecked",
                                              []
                                            |),
                                            [
                                              M.read (| raw_arr |);
                                              Value.StructRecord
                                                "core::ops::range::Range"
                                                [
                                                  ("start", Value.Integer IntegerKind.Usize 0);
                                                  ("end_", M.read (| init |))
                                                ]
                                            ]
                                          |)
                                        ]
                                    |)))
                              ]
                            |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item T A));
              ("next", InstanceField.Method (next T A));
              ("size_hint", InstanceField.Method (size_hint T A));
              ("advance_by", InstanceField.Method (advance_by T A));
              ("count", InstanceField.Method (count T A));
              ("try_fold", InstanceField.Method (try_fold T A));
              ("fold", InstanceField.Method (fold T A));
              ("last", InstanceField.Method (last T A));
              ("next_chunk", InstanceField.Method (next_chunk T A))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::into_iter::IntoIter") [] [ T; A ].
        
        (*
            fn next_back(&mut self) -> Option<T> {
                self.inner.pop_back()
            }
        *)
        Definition next_back
            (T A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                  "pop_back",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "alloc::collections::vec_deque::into_iter::IntoIter",
                    "inner"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                let len = self.inner.len;
                let rem = if len < n {
                    self.inner.clear();
                    n - len
                } else {
                    self.inner.truncate(len - n);
                    0
                };
                NonZero::new(rem).map_or(Ok(()), Err)
            }
        *)
        Definition advance_back_by
            (T A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.read (|
                let~ len :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "alloc::collections::vec_deque::into_iter::IntoIter",
                        "inner"
                      |),
                      "alloc::collections::vec_deque::VecDeque",
                      "len"
                    |)
                  |) in
                let~ rem :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (| BinOp.lt (| M.read (| len |), M.read (| n |) |) |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::vec_deque::VecDeque")
                                      []
                                      [ T; A ],
                                    "clear",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "alloc::collections::vec_deque::into_iter::IntoIter",
                                      "inner"
                                    |)
                                  ]
                                |)
                              |) in
                            M.alloc (| BinOp.Wrap.sub (| M.read (| n |), M.read (| len |) |) |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::vec_deque::VecDeque")
                                      []
                                      [ T; A ],
                                    "truncate",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "alloc::collections::vec_deque::into_iter::IntoIter",
                                      "inner"
                                    |);
                                    BinOp.Wrap.sub (| M.read (| len |), M.read (| n |) |)
                                  ]
                                |)
                              |) in
                            M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ],
                      "map_or",
                      [
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [
                            Ty.tuple [];
                            Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                          ];
                        Ty.function
                          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                          ]
                          (Ty.apply
                            (Ty.path "core::result::Result")
                            []
                            [
                              Ty.tuple [];
                              Ty.apply
                                (Ty.path "core::num::nonzero::NonZero")
                                []
                                [ Ty.path "usize" ]
                            ])
                      ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                          "new",
                          []
                        |),
                        [ M.read (| rem |) ]
                      |);
                      Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ];
                      M.constructor_as_closure "core::result::Result::Err"
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_rfold<B, F, R>(&mut self, mut init: B, mut f: F) -> R
            where
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                struct Guard<'a, T, A: Allocator> {
                    deque: &'a mut VecDeque<T, A>,
                    // `consumed <= deque.len` always holds.
                    consumed: usize,
                }
        
                impl<'a, T, A: Allocator> Drop for Guard<'a, T, A> {
                    fn drop(&mut self) {
                        self.deque.len -= self.consumed;
                    }
                }
        
                let mut guard = Guard { deque: &mut self.inner, consumed: 0 };
        
                let (head, tail) = guard.deque.as_slices();
        
                init = tail
                    .iter()
                    .map(|elem| {
                        guard.consumed += 1;
                        // SAFETY: See `try_fold`'s safety comment.
                        unsafe { ptr::read(elem) }
                    })
                    .try_rfold(init, &mut f)?;
        
                head.iter()
                    .map(|elem| {
                        guard.consumed += 1;
                        // SAFETY: Same as above.
                        unsafe { ptr::read(elem) }
                    })
                    .try_rfold(init, &mut f)
            }
        *)
        Definition try_rfold
            (T A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [ B; F; R ], [ 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~ guard :=
                      M.alloc (|
                        Value.StructRecord
                          "alloc::collections::vec_deque::into_iter::try_rfold::Guard"
                          [
                            ("deque",
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::vec_deque::into_iter::IntoIter",
                                "inner"
                              |));
                            ("consumed", Value.Integer IntegerKind.Usize 0)
                          ]
                      |) in
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::vec_deque::VecDeque")
                              []
                              [ T; A ],
                            "as_slices",
                            []
                          |),
                          [
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                guard,
                                "alloc::collections::vec_deque::into_iter::try_rfold::Guard",
                                "deque"
                              |)
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let head := M.copy (| γ0_0 |) in
                            let tail := M.copy (| γ0_1 |) in
                            let~ _ :=
                              M.write (|
                                init,
                                M.read (|
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::try_trait::Try",
                                          R,
                                          [],
                                          "branch",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::double_ended::DoubleEndedIterator",
                                              Ty.apply
                                                (Ty.path "core::iter::adapters::map::Map")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::slice::iter::Iter")
                                                    []
                                                    [ T ];
                                                  Ty.function
                                                    [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ]
                                                    T
                                                ],
                                              [],
                                              "try_rfold",
                                              [ B; Ty.apply (Ty.path "&mut") [] [ F ]; R ]
                                            |),
                                            [
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::iter::traits::iterator::Iterator",
                                                    Ty.apply
                                                      (Ty.path "core::slice::iter::Iter")
                                                      []
                                                      [ T ],
                                                    [],
                                                    "map",
                                                    [
                                                      T;
                                                      Ty.function
                                                        [
                                                          Ty.tuple
                                                            [ Ty.apply (Ty.path "&") [] [ T ] ]
                                                        ]
                                                        T
                                                    ]
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply (Ty.path "slice") [] [ T ],
                                                        "iter",
                                                        []
                                                      |),
                                                      [ M.read (| tail |) ]
                                                    |);
                                                    M.closure
                                                      (fun γ =>
                                                        ltac:(M.monadic
                                                          match γ with
                                                          | [ α0 ] =>
                                                            ltac:(M.monadic
                                                              (M.match_operator (|
                                                                M.alloc (| α0 |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let elem := M.copy (| γ |) in
                                                                      M.read (|
                                                                        let~ _ :=
                                                                          let β :=
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              guard,
                                                                              "alloc::collections::vec_deque::into_iter::try_rfold::Guard",
                                                                              "consumed"
                                                                            |) in
                                                                          M.write (|
                                                                            β,
                                                                            BinOp.Wrap.add (|
                                                                              M.read (| β |),
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                1
                                                                            |)
                                                                          |) in
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_function (|
                                                                              "core::ptr::read",
                                                                              [ T ]
                                                                            |),
                                                                            [ M.read (| elem |) ]
                                                                          |)
                                                                        |)
                                                                      |)))
                                                                ]
                                                              |)))
                                                          | _ =>
                                                            M.impossible "wrong number of arguments"
                                                          end))
                                                  ]
                                                |)
                                              |);
                                              M.read (| init |);
                                              f
                                            ]
                                          |)
                                        ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::ops::control_flow::ControlFlow::Break",
                                              0
                                            |) in
                                          let residual := M.copy (| γ0_0 |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                M.return_ (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::FromResidual",
                                                      R,
                                                      [ Ty.associated ],
                                                      "from_residual",
                                                      []
                                                    |),
                                                    [ M.read (| residual |) ]
                                                  |)
                                                |)
                                              |)
                                            |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::ops::control_flow::ControlFlow::Continue",
                                              0
                                            |) in
                                          let val := M.copy (| γ0_0 |) in
                                          val))
                                    ]
                                  |)
                                |)
                              |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::double_ended::DoubleEndedIterator",
                                  Ty.apply
                                    (Ty.path "core::iter::adapters::map::Map")
                                    []
                                    [
                                      Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ];
                                      Ty.function [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ] T
                                    ],
                                  [],
                                  "try_rfold",
                                  [ B; Ty.apply (Ty.path "&mut") [] [ F ]; R ]
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                        [],
                                        "map",
                                        [
                                          T;
                                          Ty.function
                                            [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ]
                                            T
                                        ]
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "slice") [] [ T ],
                                            "iter",
                                            []
                                          |),
                                          [ M.read (| head |) ]
                                        |);
                                        M.closure
                                          (fun γ =>
                                            ltac:(M.monadic
                                              match γ with
                                              | [ α0 ] =>
                                                ltac:(M.monadic
                                                  (M.match_operator (|
                                                    M.alloc (| α0 |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let elem := M.copy (| γ |) in
                                                          M.read (|
                                                            let~ _ :=
                                                              let β :=
                                                                M.SubPointer.get_struct_record_field (|
                                                                  guard,
                                                                  "alloc::collections::vec_deque::into_iter::try_rfold::Guard",
                                                                  "consumed"
                                                                |) in
                                                              M.write (|
                                                                β,
                                                                BinOp.Wrap.add (|
                                                                  M.read (| β |),
                                                                  Value.Integer IntegerKind.Usize 1
                                                                |)
                                                              |) in
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::ptr::read",
                                                                  [ T ]
                                                                |),
                                                                [ M.read (| elem |) ]
                                                              |)
                                                            |)
                                                          |)))
                                                    ]
                                                  |)))
                                              | _ => M.impossible "wrong number of arguments"
                                              end))
                                      ]
                                    |)
                                  |);
                                  M.read (| init |);
                                  f
                                ]
                              |)
                            |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn rfold<B, F>(mut self, init: B, mut f: F) -> B
            where
                F: FnMut(B, Self::Item) -> B,
            {
                match self.try_rfold(init, |b, item| Ok::<B, !>(f(b, item))) {
                    Ok(b) => b,
                }
            }
        *)
        Definition rfold (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T A 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.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::double_ended::DoubleEndedIterator",
                        Ty.apply
                          (Ty.path "alloc::collections::vec_deque::into_iter::IntoIter")
                          []
                          [ T; A ],
                        [],
                        "try_rfold",
                        [
                          B;
                          Ty.function
                            [ Ty.tuple [ B; T ] ]
                            (Ty.apply (Ty.path "core::result::Result") [] [ B; Ty.path "never" ]);
                          Ty.apply (Ty.path "core::result::Result") [] [ B; Ty.path "never" ]
                        ]
                      |),
                      [
                        self;
                        M.read (| init |);
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [ α0; α1 ] =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let b := M.copy (| γ |) in
                                          M.match_operator (|
                                            M.alloc (| α1 |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let item := M.copy (| γ |) in
                                                  Value.StructTuple
                                                    "core::result::Result::Ok"
                                                    [
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::function::FnMut",
                                                          F,
                                                          [ Ty.tuple [ B; T ] ],
                                                          "call_mut",
                                                          []
                                                        |),
                                                        [
                                                          f;
                                                          Value.Tuple
                                                            [ M.read (| b |); M.read (| item |) ]
                                                        ]
                                                      |)
                                                    ]))
                                            ]
                                          |)))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::result::Result::Ok",
                            0
                          |) in
                        let b := M.copy (| γ0_0 |) in
                        b))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::double_ended::DoubleEndedIterator"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("next_back", InstanceField.Method (next_back T A));
              ("advance_back_by", InstanceField.Method (advance_back_by T A));
              ("try_rfold", InstanceField.Method (try_rfold T A));
              ("rfold", InstanceField.Method (rfold T A))
            ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
      
      Module Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::into_iter::IntoIter") [] [ T; A ].
        
        (*
            fn is_empty(&self) -> bool {
                self.inner.is_empty()
            }
        *)
        Definition is_empty
            (T A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                  "is_empty",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "alloc::collections::vec_deque::into_iter::IntoIter",
                    "inner"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::exact_size::ExactSizeIterator"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("is_empty", InstanceField.Method (is_empty T A)) ].
      End Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::into_iter::IntoIter") [] [ T; A ].
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::FusedIterator"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_FusedIterator_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
      
      Module Impl_core_iter_traits_marker_TrustedLen_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
        Definition Self (T A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::collections::vec_deque::into_iter::IntoIter") [] [ T; A ].
        
        Axiom Implements :
          forall (T A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::TrustedLen"
            (Self T A)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_TrustedLen_where_core_alloc_Allocator_A_for_alloc_collections_vec_deque_into_iter_IntoIter_T_A.
    End into_iter.
  End vec_deque.
End collections.
