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

Module iter.
  Module adapters.
    Module enumerate.
      (* StructRecord
        {
          name := "Enumerate";
          const_params := [];
          ty_params := [ "I" ];
          fields := [ ("iter", I); ("count", Ty.path "usize") ];
        } *)
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        (* Clone *)
        Definition clone (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructRecord
                "core::iter::adapters::enumerate::Enumerate"
                [
                  ("iter",
                    M.call_closure (|
                      M.get_trait_method (| "core::clone::Clone", I, [], "clone", [] |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::enumerate::Enumerate",
                          "iter"
                        |)
                      ]
                    |));
                  ("count",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "usize",
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::enumerate::Enumerate",
                          "count"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::clone::Clone"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method (clone I)) ].
      End Impl_core_clone_Clone_where_core_clone_Clone_I_for_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        (* Debug *)
        Definition fmt (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "debug_struct_field2_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "Enumerate" |);
                  M.read (| Value.String "iter" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::enumerate::Enumerate",
                    "iter"
                  |);
                  M.read (| Value.String "count" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::enumerate::Enumerate",
                      "count"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::fmt::Debug"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method (fmt I)) ].
      End Impl_core_fmt_Debug_where_core_fmt_Debug_I_for_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        (*
            pub(in crate::iter) fn new(iter: I) -> Enumerate<I> {
                Enumerate { iter, count: 0 }
            }
        *)
        Definition new (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ iter ] =>
            ltac:(M.monadic
              (let iter := M.alloc (| iter |) in
              Value.StructRecord
                "core::iter::adapters::enumerate::Enumerate"
                [ ("iter", M.read (| iter |)); ("count", Value.Integer IntegerKind.Usize 0) ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (I : Ty.t),
          M.IsAssociatedFunction (Self I) "new" (new I).
      End Impl_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        (*     type Item = (usize, <I as Iterator>::Item); *)
        Definition _Item (I : Ty.t) : Ty.t := Ty.tuple [ Ty.path "usize"; Ty.associated ].
        
        (*
            fn next(&mut self) -> Option<(usize, <I as Iterator>::Item)> {
                let a = self.iter.next()?;
                let i = self.count;
                self.count += 1;
                Some((i, a))
            }
        *)
        Definition next (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ a :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    I,
                                    [],
                                    "next",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::adapters::enumerate::Enumerate",
                                      "iter"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.tuple [ Ty.path "usize"; Ty.associated ] ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "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
                    let~ i :=
                      M.copy (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::enumerate::Enumerate",
                          "count"
                        |)
                      |) in
                    let~ _ :=
                      let β :=
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::enumerate::Enumerate",
                          "count"
                        |) in
                      M.write (|
                        β,
                        BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.Usize 1 |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [ Value.Tuple [ M.read (| i |); M.read (| a |) ] ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                self.iter.size_hint()
            }
        *)
        Definition size_hint (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "size_hint",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::enumerate::Enumerate",
                    "iter"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth(&mut self, n: usize) -> Option<(usize, I::Item)> {
                let a = self.iter.nth(n)?;
                let i = self.count + n;
                self.count = i + 1;
                Some((i, a))
            }
        *)
        Definition nth (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ a :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    I,
                                    [],
                                    "nth",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::adapters::enumerate::Enumerate",
                                      "iter"
                                    |);
                                    M.read (| n |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.tuple [ Ty.path "usize"; Ty.associated ] ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "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
                    let~ i :=
                      M.alloc (|
                        BinOp.Wrap.add (|
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::iter::adapters::enumerate::Enumerate",
                              "count"
                            |)
                          |),
                          M.read (| n |)
                        |)
                      |) in
                    let~ _ :=
                      M.write (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::enumerate::Enumerate",
                          "count"
                        |),
                        BinOp.Wrap.add (| M.read (| i |), Value.Integer IntegerKind.Usize 1 |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [ Value.Tuple [ M.read (| i |); M.read (| a |) ] ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn count(self) -> usize {
                self.iter.count()
            }
        *)
        Definition count (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "count",
                  []
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::iter::adapters::enumerate::Enumerate",
                      "iter"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_fold<Acc, Fold, R>(&mut self, init: Acc, fold: Fold) -> R
            where
                Self: Sized,
                Fold: FnMut(Acc, Self::Item) -> R,
                R: Try<Output = Acc>,
            {
                #[inline]
                fn enumerate<'a, T, Acc, R>(
                    count: &'a mut usize,
                    mut fold: impl FnMut(Acc, (usize, T)) -> R + 'a,
                ) -> impl FnMut(Acc, T) -> R + 'a {
                    #[rustc_inherit_overflow_checks]
                    move |acc, item| {
                        let acc = fold(acc, ( *count, item));
                        *count += 1;
                        acc
                    }
                }
        
                self.iter.try_fold(init, enumerate(&mut self.count, fold))
            }
        *)
        Definition try_fold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ Acc; Fold; R ], [ self; init; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let fold := M.alloc (| fold |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "try_fold",
                  [ Acc; Ty.associated; R ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::enumerate::Enumerate",
                    "iter"
                  |);
                  M.read (| init |);
                  M.call_closure (|
                    M.get_associated_function (| Self, "enumerate.try_fold", [] |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::adapters::enumerate::Enumerate",
                        "count"
                      |);
                      M.read (| fold |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn fold<Acc, Fold>(self, init: Acc, fold: Fold) -> Acc
            where
                Fold: FnMut(Acc, Self::Item) -> Acc,
            {
                #[inline]
                fn enumerate<T, Acc>(
                    mut count: usize,
                    mut fold: impl FnMut(Acc, (usize, T)) -> Acc,
                ) -> impl FnMut(Acc, T) -> Acc {
                    #[rustc_inherit_overflow_checks]
                    move |acc, item| {
                        let acc = fold(acc, (count, item));
                        count += 1;
                        acc
                    }
                }
        
                self.iter.fold(init, enumerate(self.count, fold))
            }
        *)
        Definition fold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ Acc; Fold ], [ self; init; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let fold := M.alloc (| fold |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "fold",
                  [ Acc; Ty.associated ]
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::iter::adapters::enumerate::Enumerate",
                      "iter"
                    |)
                  |);
                  M.read (| init |);
                  M.call_closure (|
                    M.get_associated_function (| Self, "enumerate.fold", [] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::iter::adapters::enumerate::Enumerate",
                          "count"
                        |)
                      |);
                      M.read (| fold |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                let remaining = self.iter.advance_by(n);
                let advanced = match remaining {
                    Ok(()) => n,
                    Err(rem) => n - rem.get(),
                };
                self.count += advanced;
                remaining
            }
        *)
        Definition advance_by
            (I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.read (|
                let~ remaining :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        I,
                        [],
                        "advance_by",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::enumerate::Enumerate",
                          "iter"
                        |);
                        M.read (| n |)
                      ]
                    |)
                  |) in
                let~ advanced :=
                  M.copy (|
                    M.match_operator (|
                      remaining,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Ok",
                                0
                              |) in
                            n));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Err",
                                0
                              |) in
                            let rem := M.copy (| γ0_0 |) in
                            M.alloc (|
                              BinOp.Wrap.sub (|
                                M.read (| n |),
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::num::nonzero::NonZero")
                                      []
                                      [ Ty.path "usize" ],
                                    "get",
                                    []
                                  |),
                                  [ M.read (| rem |) ]
                                |)
                              |)
                            |)))
                      ]
                    |)
                  |) in
                let~ _ :=
                  let β :=
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::enumerate::Enumerate",
                      "count"
                    |) in
                  M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| advanced |) |) |) in
                remaining
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> <Self as Iterator>::Item
            where
                Self: TrustedRandomAccessNoCoerce,
            {
                // SAFETY: the caller must uphold the contract for
                // `Iterator::__iterator_get_unchecked`.
                let value = unsafe { try_get_unchecked(&mut self.iter, idx) };
                (self.count + idx, value)
            }
        *)
        Definition __iterator_get_unchecked
            (I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; idx ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let idx := M.alloc (| idx |) in
              M.read (|
                let~ value :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::iter::adapters::zip::try_get_unchecked", [ I ] |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::enumerate::Enumerate",
                          "iter"
                        |);
                        M.read (| idx |)
                      ]
                    |)
                  |) in
                M.alloc (|
                  Value.Tuple
                    [
                      BinOp.Wrap.add (|
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::iter::adapters::enumerate::Enumerate",
                            "count"
                          |)
                        |),
                        M.read (| idx |)
                      |);
                      M.read (| value |)
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item I));
              ("next", InstanceField.Method (next I));
              ("size_hint", InstanceField.Method (size_hint I));
              ("nth", InstanceField.Method (nth I));
              ("count", InstanceField.Method (count I));
              ("try_fold", InstanceField.Method (try_fold I));
              ("fold", InstanceField.Method (fold I));
              ("advance_by", InstanceField.Method (advance_by I));
              ("__iterator_get_unchecked", InstanceField.Method (__iterator_get_unchecked I))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_for_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_iter_traits_exact_size_ExactSizeIterator_I_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        (*
            fn next_back(&mut self) -> Option<(usize, <I as Iterator>::Item)> {
                let a = self.iter.next_back()?;
                let len = self.iter.len();
                // Can safely add, `ExactSizeIterator` promises that the number of
                // elements fits into a `usize`.
                Some((self.count + len, a))
            }
        *)
        Definition next_back (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ a :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::double_ended::DoubleEndedIterator",
                                    I,
                                    [],
                                    "next_back",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::adapters::enumerate::Enumerate",
                                      "iter"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.tuple [ Ty.path "usize"; Ty.associated ] ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "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
                    let~ len :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::exact_size::ExactSizeIterator",
                            I,
                            [],
                            "len",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::iter::adapters::enumerate::Enumerate",
                              "iter"
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          Value.Tuple
                            [
                              BinOp.Wrap.add (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::adapters::enumerate::Enumerate",
                                    "count"
                                  |)
                                |),
                                M.read (| len |)
                              |);
                              M.read (| a |)
                            ]
                        ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth_back(&mut self, n: usize) -> Option<(usize, <I as Iterator>::Item)> {
                let a = self.iter.nth_back(n)?;
                let len = self.iter.len();
                // Can safely add, `ExactSizeIterator` promises that the number of
                // elements fits into a `usize`.
                Some((self.count + len, a))
            }
        *)
        Definition nth_back (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ a :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::double_ended::DoubleEndedIterator",
                                    I,
                                    [],
                                    "nth_back",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::adapters::enumerate::Enumerate",
                                      "iter"
                                    |);
                                    M.read (| n |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.tuple [ Ty.path "usize"; Ty.associated ] ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "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
                    let~ len :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::exact_size::ExactSizeIterator",
                            I,
                            [],
                            "len",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::iter::adapters::enumerate::Enumerate",
                              "iter"
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          Value.Tuple
                            [
                              BinOp.Wrap.add (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::adapters::enumerate::Enumerate",
                                    "count"
                                  |)
                                |),
                                M.read (| len |)
                              |);
                              M.read (| a |)
                            ]
                        ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_rfold<Acc, Fold, R>(&mut self, init: Acc, fold: Fold) -> R
            where
                Self: Sized,
                Fold: FnMut(Acc, Self::Item) -> R,
                R: Try<Output = Acc>,
            {
                // Can safely add and subtract the count, as `ExactSizeIterator` promises
                // that the number of elements fits into a `usize`.
                fn enumerate<T, Acc, R>(
                    mut count: usize,
                    mut fold: impl FnMut(Acc, (usize, T)) -> R,
                ) -> impl FnMut(Acc, T) -> R {
                    move |acc, item| {
                        count -= 1;
                        fold(acc, (count, item))
                    }
                }
        
                let count = self.count + self.iter.len();
                self.iter.try_rfold(init, enumerate(count, fold))
            }
        *)
        Definition try_rfold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ Acc; Fold; R ], [ self; init; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let fold := M.alloc (| fold |) in
              M.read (|
                let~ count :=
                  M.alloc (|
                    BinOp.Wrap.add (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::enumerate::Enumerate",
                          "count"
                        |)
                      |),
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::exact_size::ExactSizeIterator",
                          I,
                          [],
                          "len",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::iter::adapters::enumerate::Enumerate",
                            "iter"
                          |)
                        ]
                      |)
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::double_ended::DoubleEndedIterator",
                      I,
                      [],
                      "try_rfold",
                      [ Acc; Ty.associated; R ]
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::adapters::enumerate::Enumerate",
                        "iter"
                      |);
                      M.read (| init |);
                      M.call_closure (|
                        M.get_associated_function (| Self, "enumerate.try_rfold", [] |),
                        [ M.read (| count |); M.read (| fold |) ]
                      |)
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn rfold<Acc, Fold>(self, init: Acc, fold: Fold) -> Acc
            where
                Fold: FnMut(Acc, Self::Item) -> Acc,
            {
                // Can safely add and subtract the count, as `ExactSizeIterator` promises
                // that the number of elements fits into a `usize`.
                fn enumerate<T, Acc>(
                    mut count: usize,
                    mut fold: impl FnMut(Acc, (usize, T)) -> Acc,
                ) -> impl FnMut(Acc, T) -> Acc {
                    move |acc, item| {
                        count -= 1;
                        fold(acc, (count, item))
                    }
                }
        
                let count = self.count + self.iter.len();
                self.iter.rfold(init, enumerate(count, fold))
            }
        *)
        Definition rfold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ Acc; Fold ], [ self; init; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let fold := M.alloc (| fold |) in
              M.read (|
                let~ count :=
                  M.alloc (|
                    BinOp.Wrap.add (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::iter::adapters::enumerate::Enumerate",
                          "count"
                        |)
                      |),
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::exact_size::ExactSizeIterator",
                          I,
                          [],
                          "len",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            self,
                            "core::iter::adapters::enumerate::Enumerate",
                            "iter"
                          |)
                        ]
                      |)
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::double_ended::DoubleEndedIterator",
                      I,
                      [],
                      "rfold",
                      [ Acc; Ty.associated ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::iter::adapters::enumerate::Enumerate",
                          "iter"
                        |)
                      |);
                      M.read (| init |);
                      M.call_closure (|
                        M.get_associated_function (| Self, "enumerate.rfold", [] |),
                        [ M.read (| count |); M.read (| fold |) ]
                      |)
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                // we do not need to update the count since that only tallies the number of items
                // consumed from the front. consuming items from the back can never reduce that.
                self.iter.advance_back_by(n)
            }
        *)
        Definition advance_back_by
            (I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  I,
                  [],
                  "advance_back_by",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::enumerate::Enumerate",
                    "iter"
                  |);
                  M.read (| n |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::double_ended::DoubleEndedIterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("next_back", InstanceField.Method (next_back I));
              ("nth_back", InstanceField.Method (nth_back I));
              ("try_rfold", InstanceField.Method (try_rfold I));
              ("rfold", InstanceField.Method (rfold I));
              ("advance_back_by", InstanceField.Method (advance_back_by I))
            ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_iter_traits_exact_size_ExactSizeIterator_I_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_iter_traits_exact_size_ExactSizeIterator_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        (*
            fn len(&self) -> usize {
                self.iter.len()
            }
        *)
        Definition len (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::exact_size::ExactSizeIterator",
                  I,
                  [],
                  "len",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::enumerate::Enumerate",
                    "iter"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn is_empty(&self) -> bool {
                self.iter.is_empty()
            }
        *)
        Definition is_empty (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::exact_size::ExactSizeIterator",
                  I,
                  [],
                  "is_empty",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::enumerate::Enumerate",
                    "iter"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::exact_size::ExactSizeIterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("len", InstanceField.Method (len I)); ("is_empty", InstanceField.Method (is_empty I))
            ].
      End Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_iter_traits_exact_size_ExactSizeIterator_I_for_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_iter_adapters_zip_TrustedRandomAccess_where_core_iter_adapters_zip_TrustedRandomAccess_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::zip::TrustedRandomAccess"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_adapters_zip_TrustedRandomAccess_where_core_iter_adapters_zip_TrustedRandomAccess_I_for_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_where_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        (*     const MAY_HAVE_SIDE_EFFECT: bool = I::MAY_HAVE_SIDE_EFFECT; *)
        (* Ty.path "bool" *)
        Definition value_MAY_HAVE_SIDE_EFFECT (I : Ty.t) : Value.t :=
          let Self : Ty.t := Self I in
          M.run
            ltac:(M.monadic
              (M.get_constant (|
                "core::iter::adapters::zip::TrustedRandomAccessNoCoerce::MAY_HAVE_SIDE_EFFECT"
              |))).
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::zip::TrustedRandomAccessNoCoerce"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("value_MAY_HAVE_SIDE_EFFECT", InstanceField.Constant (value_MAY_HAVE_SIDE_EFFECT I))
            ].
      End Impl_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_where_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_I_for_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_marker_FusedIterator_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::FusedIterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_marker_FusedIterator_I_for_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_iter_traits_marker_TrustedFused_where_core_iter_traits_marker_TrustedFused_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::TrustedFused"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_TrustedFused_where_core_iter_traits_marker_TrustedFused_I_for_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_iter_traits_marker_TrustedLen_where_core_iter_traits_marker_TrustedLen_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::TrustedLen"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_TrustedLen_where_core_iter_traits_marker_TrustedLen_I_for_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_iter_adapters_SourceIter_where_core_iter_adapters_SourceIter_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        (*     type Source = I::Source; *)
        Definition _Source (I : Ty.t) : Ty.t := Ty.associated.
        
        (*
            unsafe fn as_inner(&mut self) -> &mut I::Source {
                // SAFETY: unsafe function forwarding to unsafe function with the same requirements
                unsafe { SourceIter::as_inner(&mut self.iter) }
            }
        *)
        Definition as_inner (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (| "core::iter::adapters::SourceIter", I, [], "as_inner", [] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::enumerate::Enumerate",
                    "iter"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::SourceIter"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Source", InstanceField.Ty (_Source I));
              ("as_inner", InstanceField.Method (as_inner I))
            ].
      End Impl_core_iter_adapters_SourceIter_where_core_iter_adapters_SourceIter_I_for_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_iter_traits_marker_InPlaceIterable_where_core_iter_traits_marker_InPlaceIterable_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        (*     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY; *)
        (* Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ] *)
        Definition value_EXPAND_BY (I : Ty.t) : Value.t :=
          let Self : Ty.t := Self I in
          M.run
            ltac:(M.monadic
              (M.get_constant (| "core::iter::traits::marker::InPlaceIterable::EXPAND_BY" |))).
        
        (*     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY; *)
        (* Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ] *)
        Definition value_MERGE_BY (I : Ty.t) : Value.t :=
          let Self : Ty.t := Self I in
          M.run
            ltac:(M.monadic
              (M.get_constant (| "core::iter::traits::marker::InPlaceIterable::MERGE_BY" |))).
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::InPlaceIterable"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("value_EXPAND_BY", InstanceField.Constant (value_EXPAND_BY I));
              ("value_MERGE_BY", InstanceField.Constant (value_MERGE_BY I))
            ].
      End Impl_core_iter_traits_marker_InPlaceIterable_where_core_iter_traits_marker_InPlaceIterable_I_for_core_iter_adapters_enumerate_Enumerate_I.
      
      Module Impl_core_default_Default_where_core_default_Default_I_for_core_iter_adapters_enumerate_Enumerate_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ].
        
        (*
            fn default() -> Self {
                Enumerate::new(Default::default())
            }
        *)
        Definition default (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::enumerate::Enumerate") [] [ I ],
                  "new",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (| "core::default::Default", I, [], "default", [] |),
                    []
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::default::Default"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method (default I)) ].
      End Impl_core_default_Default_where_core_default_Default_I_for_core_iter_adapters_enumerate_Enumerate_I.
    End enumerate.
  End adapters.
End iter.
