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

Module iter.
  Module adapters.
    Module peekable.
      (* StructRecord
        {
          name := "Peekable";
          const_params := [];
          ty_params := [ "I" ];
          fields :=
            [
              ("iter", I);
              ("peeked",
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ] ])
            ];
        } *)
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_I_where_core_iter_traits_iterator_Iterator_I_where_core_clone_Clone_associated_type_for_core_iter_adapters_peekable_Peekable_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ 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::peekable::Peekable"
                [
                  ("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::peekable::Peekable",
                          "iter"
                        |)
                      ]
                    |));
                  ("peeked",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ] ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::peekable::Peekable",
                          "peeked"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => 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_for_core_iter_adapters_peekable_Peekable_I.
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_I_where_core_iter_traits_iterator_Iterator_I_where_core_fmt_Debug_associated_type_for_core_iter_adapters_peekable_Peekable_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ 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 "Peekable" |);
                  M.read (| Value.String "iter" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::peekable::Peekable",
                    "iter"
                  |);
                  M.read (| Value.String "peeked" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::peekable::Peekable",
                      "peeked"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => 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_fmt_Debug_associated_type_for_core_iter_adapters_peekable_Peekable_I.
      
      Module Impl_core_iter_adapters_peekable_Peekable_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ I ].
        
        (*
            pub(in crate::iter) fn new(iter: I) -> Peekable<I> {
                Peekable { iter, peeked: None }
            }
        *)
        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::peekable::Peekable"
                [
                  ("iter", M.read (| iter |));
                  ("peeked", Value.StructTuple "core::option::Option::None" [])
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (I : Ty.t),
          M.IsAssociatedFunction (Self I) "new" (new I).
        (*
            pub fn peek(&mut self) -> Option<&I::Item> {
                let iter = &mut self.iter;
                self.peeked.get_or_insert_with(|| iter.next()).as_ref()
            }
        *)
        Definition peek (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 (|
                let~ iter :=
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::peekable::Peekable",
                      "iter"
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                      "as_ref",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ] ],
                          "get_or_insert_with",
                          [
                            Ty.function
                              [ Ty.tuple [] ]
                              (Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ])
                          ]
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::iter::adapters::peekable::Peekable",
                            "peeked"
                          |);
                          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::iter::traits::iterator::Iterator",
                                                I,
                                                [],
                                                "next",
                                                []
                                              |),
                                              [ M.read (| iter |) ]
                                            |)))
                                      ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        ]
                      |)
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_peek :
          forall (I : Ty.t),
          M.IsAssociatedFunction (Self I) "peek" (peek I).
        
        (*
            pub fn peek_mut(&mut self) -> Option<&mut I::Item> {
                let iter = &mut self.iter;
                self.peeked.get_or_insert_with(|| iter.next()).as_mut()
            }
        *)
        Definition peek_mut (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 (|
                let~ iter :=
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::peekable::Peekable",
                      "iter"
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                      "as_mut",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ] ],
                          "get_or_insert_with",
                          [
                            Ty.function
                              [ Ty.tuple [] ]
                              (Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ])
                          ]
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::iter::adapters::peekable::Peekable",
                            "peeked"
                          |);
                          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::iter::traits::iterator::Iterator",
                                                I,
                                                [],
                                                "next",
                                                []
                                              |),
                                              [ M.read (| iter |) ]
                                            |)))
                                      ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        ]
                      |)
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_peek_mut :
          forall (I : Ty.t),
          M.IsAssociatedFunction (Self I) "peek_mut" (peek_mut I).
        
        (*
            pub fn next_if(&mut self, func: impl FnOnce(&I::Item) -> bool) -> Option<I::Item> {
                match self.next() {
                    Some(matched) if func(&matched) => Some(matched),
                    other => {
                        // Since we called `self.next()`, we consumed `self.peeked`.
                        assert!(self.peeked.is_none());
                        self.peeked = Some(other);
                        None
                    }
                }
            }
        *)
        Definition next_if (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ impl_FnOnce__I_Item__arrow_bool ], [ self; func ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let func := M.alloc (| func |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ I ],
                        [],
                        "next",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let matched := M.copy (| γ0_0 |) in
                        let γ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::function::FnOnce",
                                impl_FnOnce__I_Item__arrow_bool,
                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ Ty.associated ] ] ],
                                "call_once",
                                []
                              |),
                              [ M.read (| func |); Value.Tuple [ matched ] ]
                            |)
                          |) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          Value.StructTuple "core::option::Option::Some" [ M.read (| matched |) ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let other := M.copy (| γ |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [ Ty.associated ]
                                                ],
                                              "is_none",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "core::iter::adapters::peekable::Peekable",
                                                "peeked"
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.call_closure (|
                                        M.get_function (| "core::panicking::panic", [] |),
                                        [
                                          M.read (|
                                            Value.String "assertion failed: self.peeked.is_none()"
                                          |)
                                        ]
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::iter::adapters::peekable::Peekable",
                              "peeked"
                            |),
                            Value.StructTuple "core::option::Option::Some" [ M.read (| other |) ]
                          |) in
                        M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_next_if :
          forall (I : Ty.t),
          M.IsAssociatedFunction (Self I) "next_if" (next_if I).
        
        (*
            pub fn next_if_eq<T>(&mut self, expected: &T) -> Option<I::Item>
            where
                T: ?Sized,
                I::Item: PartialEq<T>,
            {
                self.next_if(|next| next == expected)
            }
        *)
        Definition next_if_eq
            (I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ T ], [ self; expected ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let expected := M.alloc (| expected |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ I ],
                  "next_if",
                  [
                    Ty.function
                      [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ Ty.associated ] ] ]
                      (Ty.path "bool")
                  ]
                |),
                [
                  M.read (| self |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let next := M.copy (| γ |) in
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply (Ty.path "&") [] [ Ty.associated ],
                                        [ Ty.apply (Ty.path "&") [] [ T ] ],
                                        "eq",
                                        []
                                      |),
                                      [ next; expected ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_next_if_eq :
          forall (I : Ty.t),
          M.IsAssociatedFunction (Self I) "next_if_eq" (next_if_eq I).
      End Impl_core_iter_adapters_peekable_Peekable_I.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_for_core_iter_adapters_peekable_Peekable_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ I ].
        
        (*     type Item = I::Item; *)
        Definition _Item (I : Ty.t) : Ty.t := Ty.associated.
        
        (*
            fn next(&mut self) -> Option<I::Item> {
                match self.peeked.take() {
                    Some(v) => v,
                    None => 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 (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ] ],
                        "take",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::peekable::Peekable",
                          "peeked"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let v := M.copy (| γ0_0 |) in
                        v));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (|
                          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::peekable::Peekable",
                                "iter"
                              |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn count(mut self) -> usize {
                match self.peeked.take() {
                    Some(None) => 0,
                    Some(Some(_)) => 1 + self.iter.count(),
                    None => 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.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ] ],
                        "take",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::iter::adapters::peekable::Peekable",
                          "peeked"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                        M.alloc (| Value.Integer IntegerKind.Usize 0 |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ0_0,
                            "core::option::Option::Some",
                            0
                          |) in
                        M.alloc (|
                          BinOp.Wrap.add (|
                            Value.Integer IntegerKind.Usize 1,
                            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::peekable::Peekable",
                                    "iter"
                                  |)
                                |)
                              ]
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (|
                          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::peekable::Peekable",
                                  "iter"
                                |)
                              |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth(&mut self, n: usize) -> Option<I::Item> {
                match self.peeked.take() {
                    Some(None) => None,
                    Some(v @ Some(_)) if n == 0 => v,
                    Some(Some(_)) => self.iter.nth(n - 1),
                    None => self.iter.nth(n),
                }
            }
        *)
        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.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ] ],
                        "take",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::peekable::Peekable",
                          "peeked"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                        M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let v := M.copy (| γ0_0 |) in
                        let γ2_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ0_0,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ :=
                          M.alloc (|
                            BinOp.eq (| M.read (| n |), Value.Integer IntegerKind.Usize 0 |)
                          |) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        v));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ0_0,
                            "core::option::Option::Some",
                            0
                          |) in
                        M.alloc (|
                          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::peekable::Peekable",
                                "iter"
                              |);
                              BinOp.Wrap.sub (| M.read (| n |), Value.Integer IntegerKind.Usize 1 |)
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (|
                          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::peekable::Peekable",
                                "iter"
                              |);
                              M.read (| n |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn last(mut self) -> Option<I::Item> {
                let peek_opt = match self.peeked.take() {
                    Some(None) => return None,
                    Some(v) => v,
                    None => None,
                };
                self.iter.last().or(peek_opt)
            }
        *)
        Definition last (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~ peek_opt :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ]
                                  ],
                                "take",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::iter::adapters::peekable::Peekable",
                                  "peeked"
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let _ :=
                                  M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        Value.StructTuple "core::option::Option::None" []
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let v := M.copy (| γ0_0 |) in
                                v));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                          "or",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              I,
                              [],
                              "last",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::iter::adapters::peekable::Peekable",
                                  "iter"
                                |)
                              |)
                            ]
                          |);
                          M.read (| peek_opt |)
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                let peek_len = match self.peeked {
                    Some(None) => return (0, Some(0)),
                    Some(Some(_)) => 1,
                    None => 0,
                };
                let (lo, hi) = self.iter.size_hint();
                let lo = lo.saturating_add(peek_len);
                let hi = match hi {
                    Some(x) => x.checked_add(peek_len),
                    None => None,
                };
                (lo, hi)
            }
        *)
        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.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ peek_len :=
                      M.copy (|
                        M.match_operator (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::iter::adapters::peekable::Peekable",
                            "peeked"
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let _ :=
                                  M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        Value.Tuple
                                          [
                                            Value.Integer IntegerKind.Usize 0;
                                            Value.StructTuple
                                              "core::option::Option::Some"
                                              [ Value.Integer IntegerKind.Usize 0 ]
                                          ]
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ0_0,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                M.alloc (| Value.Integer IntegerKind.Usize 1 |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                          ]
                        |)
                      |) in
                    M.match_operator (|
                      M.alloc (|
                        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::peekable::Peekable",
                              "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
                            let~ lo :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "usize",
                                    "saturating_add",
                                    []
                                  |),
                                  [ M.read (| lo |); M.read (| peek_len |) ]
                                |)
                              |) in
                            let~ hi :=
                              M.copy (|
                                M.match_operator (|
                                  hi,
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::option::Option::Some",
                                            0
                                          |) in
                                        let x := M.copy (| γ0_0 |) in
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "usize",
                                              "checked_add",
                                              []
                                            |),
                                            [ M.read (| x |); M.read (| peek_len |) ]
                                          |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                        M.alloc (|
                                          Value.StructTuple "core::option::Option::None" []
                                        |)))
                                  ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [ M.read (| lo |); M.read (| hi |) ] |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_fold<B, F, R>(&mut self, init: B, mut f: F) -> R
            where
                Self: Sized,
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                let acc = match self.peeked.take() {
                    Some(None) => return try { init },
                    Some(Some(v)) => f(init, v)?,
                    None => init,
                };
                self.iter.try_fold(acc, f)
            }
        *)
        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
          | [], [ B; F; R ], [ self; init; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let f := M.alloc (| f |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ acc :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ]
                                  ],
                                "take",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::iter::adapters::peekable::Peekable",
                                  "peeked"
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let _ :=
                                  M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::Try",
                                            R,
                                            [],
                                            "from_output",
                                            []
                                          |),
                                          [ M.read (| init |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ0_0,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let v := M.copy (| γ1_0 |) in
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::Try",
                                        R,
                                        [],
                                        "branch",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::function::FnMut",
                                            F,
                                            [ Ty.tuple [ B; Ty.associated ] ],
                                            "call_mut",
                                            []
                                          |),
                                          [ f; Value.Tuple [ M.read (| init |); M.read (| v |) ] ]
                                        |)
                                      ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::ops::control_flow::ControlFlow::Break",
                                            0
                                          |) in
                                        let residual := M.copy (| γ0_0 |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.return_ (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::try_trait::FromResidual",
                                                    R,
                                                    [ Ty.associated ],
                                                    "from_residual",
                                                    []
                                                  |),
                                                  [ M.read (| residual |) ]
                                                |)
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::ops::control_flow::ControlFlow::Continue",
                                            0
                                          |) in
                                        let val := M.copy (| γ0_0 |) in
                                        val))
                                  ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                init))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::iterator::Iterator",
                          I,
                          [],
                          "try_fold",
                          [ B; F; R ]
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::iter::adapters::peekable::Peekable",
                            "iter"
                          |);
                          M.read (| acc |);
                          M.read (| f |)
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn fold<Acc, Fold>(self, init: Acc, mut fold: Fold) -> Acc
            where
                Fold: FnMut(Acc, Self::Item) -> Acc,
            {
                let acc = match self.peeked {
                    Some(None) => return init,
                    Some(Some(v)) => fold(init, v),
                    None => init,
                };
                self.iter.fold(acc, 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.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ acc :=
                      M.copy (|
                        M.match_operator (|
                          M.SubPointer.get_struct_record_field (|
                            self,
                            "core::iter::adapters::peekable::Peekable",
                            "peeked"
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let _ :=
                                  M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (| M.return_ (| M.read (| init |) |) |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ0_0,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let v := M.copy (| γ1_0 |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::function::FnMut",
                                      Fold,
                                      [ Ty.tuple [ Acc; Ty.associated ] ],
                                      "call_mut",
                                      []
                                    |),
                                    [ fold; Value.Tuple [ M.read (| init |); M.read (| v |) ] ]
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                init))
                          ]
                        |)
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::iterator::Iterator",
                          I,
                          [],
                          "fold",
                          [ Acc; Fold ]
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::iter::adapters::peekable::Peekable",
                              "iter"
                            |)
                          |);
                          M.read (| acc |);
                          M.read (| fold |)
                        ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => 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));
              ("count", InstanceField.Method (count I));
              ("nth", InstanceField.Method (nth I));
              ("last", InstanceField.Method (last I));
              ("size_hint", InstanceField.Method (size_hint I));
              ("try_fold", InstanceField.Method (try_fold I));
              ("fold", InstanceField.Method (fold I))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_for_core_iter_adapters_peekable_Peekable_I.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_peekable_Peekable_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ I ].
        
        (*
            fn next_back(&mut self) -> Option<Self::Item> {
                match self.peeked.as_mut() {
                    Some(v @ Some(_)) => self.iter.next_back().or_else(|| v.take()),
                    Some(None) => None,
                    None => self.iter.next_back(),
                }
            }
        *)
        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.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ] ],
                        "as_mut",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::peekable::Peekable",
                          "peeked"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let v := M.copy (| γ0_0 |) in
                        let γ0_0 := M.read (| γ0_0 |) in
                        let γ3_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ0_0,
                            "core::option::Option::Some",
                            0
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                              "or_else",
                              [
                                Ty.function
                                  [ Ty.tuple [] ]
                                  (Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ])
                              ]
                            |),
                            [
                              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::peekable::Peekable",
                                    "iter"
                                  |)
                                ]
                              |);
                              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_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "core::option::Option")
                                                      []
                                                      [ Ty.associated ],
                                                    "take",
                                                    []
                                                  |),
                                                  [ M.read (| v |) ]
                                                |)))
                                          ]
                                        |)))
                                    | _ => M.impossible "wrong number of arguments"
                                    end))
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ0_0 := M.read (| γ0_0 |) in
                        let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                        M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (|
                          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::peekable::Peekable",
                                "iter"
                              |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_rfold<B, F, R>(&mut self, init: B, mut f: F) -> R
            where
                Self: Sized,
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                match self.peeked.take() {
                    Some(None) => try { init },
                    Some(Some(v)) => match self.iter.try_rfold(init, &mut f).branch() {
                        ControlFlow::Continue(acc) => f(acc, v),
                        ControlFlow::Break(r) => {
                            self.peeked = Some(Some(v));
                            R::from_residual(r)
                        }
                    },
                    None => self.iter.try_rfold(init, f),
                }
            }
        *)
        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
          | [], [ B; F; R ], [ self; init; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let f := M.alloc (| f |) in
              M.read (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ] ],
                        "take",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::peekable::Peekable",
                          "peeked"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              R,
                              [],
                              "from_output",
                              []
                            |),
                            [ M.read (| init |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ0_0,
                            "core::option::Option::Some",
                            0
                          |) in
                        let v := M.copy (| γ1_0 |) in
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                R,
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::double_ended::DoubleEndedIterator",
                                    I,
                                    [],
                                    "try_rfold",
                                    [ B; Ty.apply (Ty.path "&mut") [] [ F ]; R ]
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::adapters::peekable::Peekable",
                                      "iter"
                                    |);
                                    M.read (| init |);
                                    f
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let acc := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::function::FnMut",
                                      F,
                                      [ Ty.tuple [ B; Ty.associated ] ],
                                      "call_mut",
                                      []
                                    |),
                                    [ f; Value.Tuple [ M.read (| acc |); M.read (| v |) ] ]
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let r := M.copy (| γ0_0 |) in
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::adapters::peekable::Peekable",
                                      "peeked"
                                    |),
                                    Value.StructTuple
                                      "core::option::Option::Some"
                                      [
                                        Value.StructTuple
                                          "core::option::Option::Some"
                                          [ M.read (| v |) ]
                                      ]
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::try_trait::FromResidual",
                                      R,
                                      [ Ty.associated ],
                                      "from_residual",
                                      []
                                    |),
                                    [ M.read (| r |) ]
                                  |)
                                |)))
                          ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::double_ended::DoubleEndedIterator",
                              I,
                              [],
                              "try_rfold",
                              [ B; F; R ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::iter::adapters::peekable::Peekable",
                                "iter"
                              |);
                              M.read (| init |);
                              M.read (| f |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn rfold<Acc, Fold>(self, init: Acc, mut fold: Fold) -> Acc
            where
                Fold: FnMut(Acc, Self::Item) -> Acc,
            {
                match self.peeked {
                    Some(None) => init,
                    Some(Some(v)) => {
                        let acc = self.iter.rfold(init, &mut fold);
                        fold(acc, v)
                    }
                    None => self.iter.rfold(init, 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 (|
                M.match_operator (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::iter::adapters::peekable::Peekable",
                    "peeked"
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                        init));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ0_0,
                            "core::option::Option::Some",
                            0
                          |) in
                        let v := M.copy (| γ1_0 |) in
                        let~ acc :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::double_ended::DoubleEndedIterator",
                                I,
                                [],
                                "rfold",
                                [ Acc; Ty.apply (Ty.path "&mut") [] [ Fold ] ]
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::iter::adapters::peekable::Peekable",
                                    "iter"
                                  |)
                                |);
                                M.read (| init |);
                                fold
                              ]
                            |)
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::function::FnMut",
                              Fold,
                              [ Ty.tuple [ Acc; Ty.associated ] ],
                              "call_mut",
                              []
                            |),
                            [ fold; Value.Tuple [ M.read (| acc |); M.read (| v |) ] ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::double_ended::DoubleEndedIterator",
                              I,
                              [],
                              "rfold",
                              [ Acc; Fold ]
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::iter::adapters::peekable::Peekable",
                                  "iter"
                                |)
                              |);
                              M.read (| init |);
                              M.read (| fold |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => 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));
              ("try_rfold", InstanceField.Method (try_rfold I));
              ("rfold", InstanceField.Method (rfold I))
            ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_peekable_Peekable_I.
      
      Module Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_iter_traits_exact_size_ExactSizeIterator_I_for_core_iter_adapters_peekable_Peekable_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ I ].
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::exact_size::ExactSizeIterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_iter_traits_exact_size_ExactSizeIterator_I_for_core_iter_adapters_peekable_Peekable_I.
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_marker_FusedIterator_I_for_core_iter_adapters_peekable_Peekable_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ 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_peekable_Peekable_I.
      
      
      Module Impl_core_iter_traits_marker_TrustedLen_where_core_iter_traits_marker_TrustedLen_I_for_core_iter_adapters_peekable_Peekable_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ 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_peekable_Peekable_I.
      
      Module Impl_core_iter_adapters_SourceIter_where_core_iter_traits_iterator_Iterator_I_where_core_iter_adapters_SourceIter_I_for_core_iter_adapters_peekable_Peekable_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::peekable::Peekable") [] [ 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::peekable::Peekable",
                    "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_traits_iterator_Iterator_I_where_core_iter_adapters_SourceIter_I_for_core_iter_adapters_peekable_Peekable_I.
    End peekable.
  End adapters.
End iter.
