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

Module iter.
  Module adapters.
    Module intersperse.
      (* StructRecord
        {
          name := "Intersperse";
          const_params := [];
          ty_params := [ "I" ];
          fields :=
            [
              ("started", Ty.path "bool");
              ("separator", Ty.associated);
              ("next_item", Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ]);
              ("iter", Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ])
            ];
        } *)
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_I_where_core_iter_traits_iterator_Iterator_I_where_core_clone_Clone_associated_type_where_core_fmt_Debug_associated_type_where_core_fmt_Debug_associated_type_for_core_iter_adapters_intersperse_Intersperse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::intersperse::Intersperse") [] [ 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_field4_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "Intersperse" |);
                  M.read (| Value.String "started" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::intersperse::Intersperse",
                    "started"
                  |);
                  M.read (| Value.String "separator" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::intersperse::Intersperse",
                    "separator"
                  |);
                  M.read (| Value.String "next_item" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::intersperse::Intersperse",
                    "next_item"
                  |);
                  M.read (| Value.String "iter" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::intersperse::Intersperse",
                      "iter"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => 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_where_core_iter_traits_iterator_Iterator_I_where_core_clone_Clone_associated_type_where_core_fmt_Debug_associated_type_where_core_fmt_Debug_associated_type_for_core_iter_adapters_intersperse_Intersperse_I.
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_I_where_core_iter_traits_iterator_Iterator_I_where_core_clone_Clone_associated_type_where_core_clone_Clone_associated_type_where_core_clone_Clone_associated_type_for_core_iter_adapters_intersperse_Intersperse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::intersperse::Intersperse") [] [ 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::intersperse::Intersperse"
                [
                  ("started",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "bool",
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::intersperse::Intersperse",
                          "started"
                        |)
                      ]
                    |));
                  ("separator",
                    M.call_closure (|
                      M.get_trait_method (| "core::clone::Clone", Ty.associated, [], "clone", [] |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::intersperse::Intersperse",
                          "separator"
                        |)
                      ]
                    |));
                  ("next_item",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::intersperse::Intersperse",
                          "next_item"
                        |)
                      ]
                    |));
                  ("iter",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::intersperse::Intersperse",
                          "iter"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => 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_where_core_iter_traits_iterator_Iterator_I_where_core_clone_Clone_associated_type_where_core_clone_Clone_associated_type_where_core_clone_Clone_associated_type_for_core_iter_adapters_intersperse_Intersperse_I.
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_marker_FusedIterator_I_where_core_clone_Clone_associated_type_for_core_iter_adapters_intersperse_Intersperse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::intersperse::Intersperse") [] [ 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_where_core_clone_Clone_associated_type_for_core_iter_adapters_intersperse_Intersperse_I.
      
      Module Impl_core_iter_adapters_intersperse_Intersperse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::intersperse::Intersperse") [] [ I ].
        
        (*
            pub(in crate::iter) fn new(iter: I, separator: I::Item) -> Self {
                Self { started: false, separator, next_item: None, iter: iter.fuse() }
            }
        *)
        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; separator ] =>
            ltac:(M.monadic
              (let iter := M.alloc (| iter |) in
              let separator := M.alloc (| separator |) in
              Value.StructRecord
                "core::iter::adapters::intersperse::Intersperse"
                [
                  ("started", Value.Bool false);
                  ("separator", M.read (| separator |));
                  ("next_item", Value.StructTuple "core::option::Option::None" []);
                  ("iter",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        I,
                        [],
                        "fuse",
                        []
                      |),
                      [ M.read (| iter |) ]
                    |))
                ]))
          | _, _, _ => 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_intersperse_Intersperse_I.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_where_core_clone_Clone_associated_type_for_core_iter_adapters_intersperse_Intersperse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::intersperse::Intersperse") [] [ I ].
        
        (*     type Item = I::Item; *)
        Definition _Item (I : Ty.t) : Ty.t := Ty.associated.
        
        (*
            fn next(&mut self) -> Option<Self::Item> {
                if self.started {
                    if let Some(v) = self.next_item.take() {
                        Some(v)
                    } else {
                        let next_item = self.iter.next();
                        if next_item.is_some() {
                            self.next_item = next_item;
                            Some(self.separator.clone())
                        } else {
                            None
                        }
                    }
                } else {
                    self.started = true;
                    self.iter.next()
                }
            }
        *)
        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.read (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::iter::adapters::intersperse::Intersperse",
                              "started"
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [ Ty.associated ],
                                        "take",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::iter::adapters::intersperse::Intersperse",
                                          "next_item"
                                        |)
                                      ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let v := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  Value.StructTuple "core::option::Option::Some" [ M.read (| v |) ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let~ next_item :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::iter::adapters::fuse::Fuse")
                                          []
                                          [ I ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::iter::adapters::intersperse::Intersperse",
                                          "iter"
                                        |)
                                      ]
                                    |)
                                  |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [ Ty.associated ],
                                                  "is_some",
                                                  []
                                                |),
                                                [ next_item ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "core::iter::adapters::intersperse::Intersperse",
                                              "next_item"
                                            |),
                                            M.read (| next_item |)
                                          |) in
                                        M.alloc (|
                                          Value.StructTuple
                                            "core::option::Option::Some"
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::clone::Clone",
                                                  Ty.associated,
                                                  [],
                                                  "clone",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "core::iter::adapters::intersperse::Intersperse",
                                                    "separator"
                                                  |)
                                                ]
                                              |)
                                            ]
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.alloc (|
                                          Value.StructTuple "core::option::Option::None" []
                                        |)))
                                  ]
                                |)))
                          ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::iter::adapters::intersperse::Intersperse",
                              "started"
                            |),
                            Value.Bool true
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ],
                              [],
                              "next",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::iter::adapters::intersperse::Intersperse",
                                "iter"
                              |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                intersperse_size_hint(&self.iter, self.started, self.next_item.is_some())
            }
        *)
        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_function (|
                  "core::iter::adapters::intersperse::intersperse_size_hint",
                  [ Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ] ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::intersperse::Intersperse",
                    "iter"
                  |);
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::intersperse::Intersperse",
                      "started"
                    |)
                  |);
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                      "is_some",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::adapters::intersperse::Intersperse",
                        "next_item"
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn fold<B, F>(self, init: B, f: F) -> B
            where
                Self: Sized,
                F: FnMut(B, Self::Item) -> B,
            {
                let separator = self.separator;
                intersperse_fold(
                    self.iter,
                    init,
                    f,
                    move || separator.clone(),
                    self.started,
                    self.next_item,
                )
            }
        *)
        Definition fold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I 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 (|
                let~ separator :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::iter::adapters::intersperse::Intersperse",
                      "separator"
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::iter::adapters::intersperse::intersperse_fold",
                      [
                        Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ];
                        B;
                        F;
                        Ty.function [ Ty.tuple [] ] Ty.associated
                      ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::iter::adapters::intersperse::Intersperse",
                          "iter"
                        |)
                      |);
                      M.read (| init |);
                      M.read (| f |);
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [ α0 ] =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| α0 |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.call_closure (|
                                          M.get_trait_method (|
                                            "core::clone::Clone",
                                            Ty.associated,
                                            [],
                                            "clone",
                                            []
                                          |),
                                          [ separator ]
                                        |)))
                                  ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end));
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::iter::adapters::intersperse::Intersperse",
                          "started"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::iter::adapters::intersperse::Intersperse",
                          "next_item"
                        |)
                      |)
                    ]
                  |)
                |)
              |)))
          | _, _, _ => 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));
              ("fold", InstanceField.Method (fold I))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_where_core_clone_Clone_associated_type_for_core_iter_adapters_intersperse_Intersperse_I.
      
      (* StructRecord
        {
          name := "IntersperseWith";
          const_params := [];
          ty_params := [ "I"; "G" ];
          fields :=
            [
              ("started", Ty.path "bool");
              ("separator", G);
              ("next_item", Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ]);
              ("iter", Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ])
            ];
        } *)
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_marker_FusedIterator_I_where_core_ops_function_FnMut_G_Tuple__for_core_iter_adapters_intersperse_IntersperseWith_I_G.
        Definition Self (I G : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::intersperse::IntersperseWith") [] [ I; G ].
        
        Axiom Implements :
          forall (I G : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::FusedIterator"
            (Self I G)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_marker_FusedIterator_I_where_core_ops_function_FnMut_G_Tuple__for_core_iter_adapters_intersperse_IntersperseWith_I_G.
      
      Module Impl_core_fmt_Debug_where_core_iter_traits_iterator_Iterator_I_where_core_fmt_Debug_I_where_core_fmt_Debug_associated_type_where_core_fmt_Debug_G_for_core_iter_adapters_intersperse_IntersperseWith_I_G.
        Definition Self (I G : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::intersperse::IntersperseWith") [] [ I; G ].
        
        (*
            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                f.debug_struct("IntersperseWith")
                    .field("started", &self.started)
                    .field("separator", &self.separator)
                    .field("iter", &self.iter)
                    .field("next_item", &self.next_item)
                    .finish()
            }
        *)
        Definition fmt (I G : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I G 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::DebugStruct",
                  "finish",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::builders::DebugStruct",
                      "field",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::builders::DebugStruct",
                          "field",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::builders::DebugStruct",
                              "field",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::builders::DebugStruct",
                                  "field",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::Formatter",
                                        "debug_struct",
                                        []
                                      |),
                                      [ M.read (| f |); M.read (| Value.String "IntersperseWith" |)
                                      ]
                                    |)
                                  |);
                                  M.read (| Value.String "started" |);
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::adapters::intersperse::IntersperseWith",
                                    "started"
                                  |)
                                ]
                              |);
                              M.read (| Value.String "separator" |);
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::iter::adapters::intersperse::IntersperseWith",
                                "separator"
                              |)
                            ]
                          |);
                          M.read (| Value.String "iter" |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::iter::adapters::intersperse::IntersperseWith",
                            "iter"
                          |)
                        ]
                      |);
                      M.read (| Value.String "next_item" |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::adapters::intersperse::IntersperseWith",
                        "next_item"
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I G : Ty.t),
          M.IsTraitInstance
            "core::fmt::Debug"
            (Self I G)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method (fmt I G)) ].
      End Impl_core_fmt_Debug_where_core_iter_traits_iterator_Iterator_I_where_core_fmt_Debug_I_where_core_fmt_Debug_associated_type_where_core_fmt_Debug_G_for_core_iter_adapters_intersperse_IntersperseWith_I_G.
      
      Module Impl_core_clone_Clone_where_core_iter_traits_iterator_Iterator_I_where_core_clone_Clone_I_where_core_clone_Clone_associated_type_where_core_clone_Clone_G_for_core_iter_adapters_intersperse_IntersperseWith_I_G.
        Definition Self (I G : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::intersperse::IntersperseWith") [] [ I; G ].
        
        (*
            fn clone(&self) -> Self {
                Self {
                    started: self.started,
                    separator: self.separator.clone(),
                    iter: self.iter.clone(),
                    next_item: self.next_item.clone(),
                }
            }
        *)
        Definition clone (I G : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I G in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructRecord
                "core::iter::adapters::intersperse::IntersperseWith"
                [
                  ("started",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::adapters::intersperse::IntersperseWith",
                        "started"
                      |)
                    |));
                  ("separator",
                    M.call_closure (|
                      M.get_trait_method (| "core::clone::Clone", G, [], "clone", [] |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::intersperse::IntersperseWith",
                          "separator"
                        |)
                      ]
                    |));
                  ("iter",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::intersperse::IntersperseWith",
                          "iter"
                        |)
                      ]
                    |));
                  ("next_item",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::intersperse::IntersperseWith",
                          "next_item"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I G : Ty.t),
          M.IsTraitInstance
            "core::clone::Clone"
            (Self I G)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method (clone I G)) ].
      End Impl_core_clone_Clone_where_core_iter_traits_iterator_Iterator_I_where_core_clone_Clone_I_where_core_clone_Clone_associated_type_where_core_clone_Clone_G_for_core_iter_adapters_intersperse_IntersperseWith_I_G.
      
      Module Impl_core_iter_adapters_intersperse_IntersperseWith_I_G.
        Definition Self (I G : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::intersperse::IntersperseWith") [] [ I; G ].
        
        (*
            pub(in crate::iter) fn new(iter: I, separator: G) -> Self {
                Self { started: false, separator, next_item: None, iter: iter.fuse() }
            }
        *)
        Definition new (I G : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I G in
          match ε, τ, α with
          | [], [], [ iter; separator ] =>
            ltac:(M.monadic
              (let iter := M.alloc (| iter |) in
              let separator := M.alloc (| separator |) in
              Value.StructRecord
                "core::iter::adapters::intersperse::IntersperseWith"
                [
                  ("started", Value.Bool false);
                  ("separator", M.read (| separator |));
                  ("next_item", Value.StructTuple "core::option::Option::None" []);
                  ("iter",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        I,
                        [],
                        "fuse",
                        []
                      |),
                      [ M.read (| iter |) ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (I G : Ty.t),
          M.IsAssociatedFunction (Self I G) "new" (new I G).
      End Impl_core_iter_adapters_intersperse_IntersperseWith_I_G.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_where_core_ops_function_FnMut_G_Tuple__for_core_iter_adapters_intersperse_IntersperseWith_I_G.
        Definition Self (I G : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::intersperse::IntersperseWith") [] [ I; G ].
        
        (*     type Item = I::Item; *)
        Definition _Item (I G : Ty.t) : Ty.t := Ty.associated.
        
        (*
            fn next(&mut self) -> Option<Self::Item> {
                if self.started {
                    if let Some(v) = self.next_item.take() {
                        Some(v)
                    } else {
                        let next_item = self.iter.next();
                        if next_item.is_some() {
                            self.next_item = next_item;
                            Some((self.separator)())
                        } else {
                            None
                        }
                    }
                } else {
                    self.started = true;
                    self.iter.next()
                }
            }
        *)
        Definition next (I G : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I G in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::iter::adapters::intersperse::IntersperseWith",
                              "started"
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [ Ty.associated ],
                                        "take",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::iter::adapters::intersperse::IntersperseWith",
                                          "next_item"
                                        |)
                                      ]
                                    |)
                                  |) in
                                let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let v := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  Value.StructTuple "core::option::Option::Some" [ M.read (| v |) ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let~ next_item :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::iter::adapters::fuse::Fuse")
                                          []
                                          [ I ],
                                        [],
                                        "next",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::iter::adapters::intersperse::IntersperseWith",
                                          "iter"
                                        |)
                                      ]
                                    |)
                                  |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [ Ty.associated ],
                                                  "is_some",
                                                  []
                                                |),
                                                [ next_item ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "core::iter::adapters::intersperse::IntersperseWith",
                                              "next_item"
                                            |),
                                            M.read (| next_item |)
                                          |) in
                                        M.alloc (|
                                          Value.StructTuple
                                            "core::option::Option::Some"
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::function::FnMut",
                                                  G,
                                                  [ Ty.tuple [] ],
                                                  "call_mut",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "core::iter::adapters::intersperse::IntersperseWith",
                                                    "separator"
                                                  |);
                                                  Value.Tuple []
                                                ]
                                              |)
                                            ]
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.alloc (|
                                          Value.StructTuple "core::option::Option::None" []
                                        |)))
                                  ]
                                |)))
                          ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::iter::adapters::intersperse::IntersperseWith",
                              "started"
                            |),
                            Value.Bool true
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ],
                              [],
                              "next",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::iter::adapters::intersperse::IntersperseWith",
                                "iter"
                              |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                intersperse_size_hint(&self.iter, self.started, self.next_item.is_some())
            }
        *)
        Definition size_hint
            (I G : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I G in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_function (|
                  "core::iter::adapters::intersperse::intersperse_size_hint",
                  [ Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ] ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::intersperse::IntersperseWith",
                    "iter"
                  |);
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::intersperse::IntersperseWith",
                      "started"
                    |)
                  |);
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                      "is_some",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::adapters::intersperse::IntersperseWith",
                        "next_item"
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn fold<B, F>(self, init: B, f: F) -> B
            where
                Self: Sized,
                F: FnMut(B, Self::Item) -> B,
            {
                intersperse_fold(self.iter, init, f, self.separator, self.started, self.next_item)
            }
        *)
        Definition fold (I G : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I G 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.call_closure (|
                M.get_function (|
                  "core::iter::adapters::intersperse::intersperse_fold",
                  [ Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ]; B; F; G ]
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::iter::adapters::intersperse::IntersperseWith",
                      "iter"
                    |)
                  |);
                  M.read (| init |);
                  M.read (| f |);
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::iter::adapters::intersperse::IntersperseWith",
                      "separator"
                    |)
                  |);
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::iter::adapters::intersperse::IntersperseWith",
                      "started"
                    |)
                  |);
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::iter::adapters::intersperse::IntersperseWith",
                      "next_item"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I G : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self I G)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item I G));
              ("next", InstanceField.Method (next I G));
              ("size_hint", InstanceField.Method (size_hint I G));
              ("fold", InstanceField.Method (fold I G))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_where_core_ops_function_FnMut_G_Tuple__for_core_iter_adapters_intersperse_IntersperseWith_I_G.
      
      (*
      fn intersperse_size_hint<I>(iter: &I, started: bool, next_is_some: bool) -> (usize, Option<usize>)
      where
          I: Iterator,
      {
          let (lo, hi) = iter.size_hint();
          (
              lo.saturating_sub(!started as usize)
                  .saturating_add(next_is_some as usize)
                  .saturating_add(lo),
              hi.and_then(|hi| {
                  hi.saturating_sub(!started as usize)
                      .saturating_add(next_is_some as usize)
                      .checked_add(hi)
              }),
          )
      }
      *)
      Definition intersperse_size_hint (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ _ as I ], [ iter; started; next_is_some ] =>
          ltac:(M.monadic
            (let iter := M.alloc (| iter |) in
            let started := M.alloc (| started |) in
            let next_is_some := M.alloc (| next_is_some |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      I,
                      [],
                      "size_hint",
                      []
                    |),
                    [ M.read (| iter |) ]
                  |)
                |),
                [
                  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 lo := M.copy (| γ0_0 |) in
                      let hi := M.copy (| γ0_1 |) in
                      M.alloc (|
                        Value.Tuple
                          [
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "usize", "saturating_add", [] |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "usize",
                                    "saturating_add",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "usize",
                                        "saturating_sub",
                                        []
                                      |),
                                      [
                                        M.read (| lo |);
                                        M.rust_cast (UnOp.not (| M.read (| started |) |))
                                      ]
                                    |);
                                    M.rust_cast (M.read (| next_is_some |))
                                  ]
                                |);
                                M.read (| lo |)
                              ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                                "and_then",
                                [
                                  Ty.path "usize";
                                  Ty.function
                                    [ Ty.tuple [ Ty.path "usize" ] ]
                                    (Ty.apply
                                      (Ty.path "core::option::Option")
                                      []
                                      [ Ty.path "usize" ])
                                ]
                              |),
                              [
                                M.read (| hi |);
                                M.closure
                                  (fun γ =>
                                    ltac:(M.monadic
                                      match γ with
                                      | [ α0 ] =>
                                        ltac:(M.monadic
                                          (M.match_operator (|
                                            M.alloc (| α0 |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let hi := M.copy (| γ |) in
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "usize",
                                                      "checked_add",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "usize",
                                                          "saturating_add",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "usize",
                                                              "saturating_sub",
                                                              []
                                                            |),
                                                            [
                                                              M.read (| hi |);
                                                              M.rust_cast
                                                                (UnOp.not (|
                                                                  M.read (| started |)
                                                                |))
                                                            ]
                                                          |);
                                                          M.rust_cast (M.read (| next_is_some |))
                                                        ]
                                                      |);
                                                      M.read (| hi |)
                                                    ]
                                                  |)))
                                            ]
                                          |)))
                                      | _ => M.impossible "wrong number of arguments"
                                      end))
                              ]
                            |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_intersperse_size_hint :
        M.IsFunction
          "core::iter::adapters::intersperse::intersperse_size_hint"
          intersperse_size_hint.
      
      (*
      fn intersperse_fold<I, B, F, G>(
          mut iter: I,
          init: B,
          mut f: F,
          mut separator: G,
          started: bool,
          mut next_item: Option<I::Item>,
      ) -> B
      where
          I: Iterator,
          F: FnMut(B, I::Item) -> B,
          G: FnMut() -> I::Item,
      {
          let mut accum = init;
      
          let first = if started { next_item.take() } else { iter.next() };
          if let Some(x) = first {
              accum = f(accum, x);
          }
      
          iter.fold(accum, |mut accum, x| {
              accum = f(accum, separator());
              accum = f(accum, x);
              accum
          })
      }
      *)
      Definition intersperse_fold (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ _ as I; B; F; G ], [ iter; init; f; separator; started; next_item ] =>
          ltac:(M.monadic
            (let iter := M.alloc (| iter |) in
            let init := M.alloc (| init |) in
            let f := M.alloc (| f |) in
            let separator := M.alloc (| separator |) in
            let started := M.alloc (| started |) in
            let next_item := M.alloc (| next_item |) in
            M.read (|
              let~ accum := M.copy (| init |) in
              let~ first :=
                M.copy (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use started in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                                "take",
                                []
                              |),
                              [ next_item ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                I,
                                [],
                                "next",
                                []
                              |),
                              [ iter ]
                            |)
                          |)))
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := first in
                        let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let x := M.copy (| γ0_0 |) in
                        let~ _ :=
                          M.write (|
                            accum,
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::function::FnMut",
                                F,
                                [ Ty.tuple [ B; Ty.associated ] ],
                                "call_mut",
                                []
                              |),
                              [ f; Value.Tuple [ M.read (| accum |); M.read (| x |) ] ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    I,
                    [],
                    "fold",
                    [ B; Ty.function [ Ty.tuple [ B; Ty.associated ] ] B ]
                  |),
                  [
                    M.read (| iter |);
                    M.read (| accum |);
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0; α1 ] =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| α0 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let accum := M.copy (| γ |) in
                                      M.match_operator (|
                                        M.alloc (| α1 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let x := M.copy (| γ |) in
                                              M.read (|
                                                let~ _ :=
                                                  M.write (|
                                                    accum,
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::function::FnMut",
                                                        F,
                                                        [ Ty.tuple [ B; Ty.associated ] ],
                                                        "call_mut",
                                                        []
                                                      |),
                                                      [
                                                        f;
                                                        Value.Tuple
                                                          [
                                                            M.read (| accum |);
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::function::FnMut",
                                                                G,
                                                                [ Ty.tuple [] ],
                                                                "call_mut",
                                                                []
                                                              |),
                                                              [ separator; Value.Tuple [] ]
                                                            |)
                                                          ]
                                                      ]
                                                    |)
                                                  |) in
                                                let~ _ :=
                                                  M.write (|
                                                    accum,
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::function::FnMut",
                                                        F,
                                                        [ Ty.tuple [ B; Ty.associated ] ],
                                                        "call_mut",
                                                        []
                                                      |),
                                                      [
                                                        f;
                                                        Value.Tuple
                                                          [ M.read (| accum |); M.read (| x |) ]
                                                      ]
                                                    |)
                                                  |) in
                                                accum
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_intersperse_fold :
        M.IsFunction "core::iter::adapters::intersperse::intersperse_fold" intersperse_fold.
    End intersperse.
  End adapters.
End iter.
