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

Module iter.
  Module traits.
    Module double_ended.
      (* Trait *)
      Module DoubleEndedIterator.
        Definition advance_back_by
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.use
                        (M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::collect::IntoIterator",
                                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                                [],
                                "into_iter",
                                []
                              |),
                              [
                                Value.StructRecord
                                  "core::ops::range::Range"
                                  [
                                    ("start", Value.Integer IntegerKind.Usize 0);
                                    ("end_", M.read (| n |))
                                  ]
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let iter := M.copy (| γ |) in
                                M.loop (|
                                  ltac:(M.monadic
                                    (let~ _ :=
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::iterator::Iterator",
                                              Ty.apply
                                                (Ty.path "core::ops::range::Range")
                                                []
                                                [ Ty.path "usize" ],
                                              [],
                                              "next",
                                              []
                                            |),
                                            [ iter ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let _ :=
                                                M.is_struct_tuple (|
                                                  γ,
                                                  "core::option::Option::None"
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (| M.read (| M.break (||) |) |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::option::Option::Some",
                                                  0
                                                |) in
                                              let i := M.copy (| γ0_0 |) in
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "core::option::Option")
                                                                  []
                                                                  [ Ty.associated ],
                                                                "is_none",
                                                                []
                                                              |),
                                                              [
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::iter::traits::double_ended::DoubleEndedIterator",
                                                                      Self,
                                                                      [],
                                                                      "next_back",
                                                                      []
                                                                    |),
                                                                    [ M.read (| self |) ]
                                                                  |)
                                                                |)
                                                              ]
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              Value.StructTuple
                                                                "core::result::Result::Err"
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::num::nonzero::NonZero")
                                                                        []
                                                                        [ Ty.path "usize" ],
                                                                      "new_unchecked",
                                                                      []
                                                                    |),
                                                                    [
                                                                      BinOp.Wrap.sub (|
                                                                        M.read (| n |),
                                                                        M.read (| i |)
                                                                      |)
                                                                    ]
                                                                  |)
                                                                ]
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |)))
                                        ]
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                                |)))
                          ]
                        |)) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_advance_back_by :
          M.IsProvidedMethod
            "core::iter::traits::double_ended::DoubleEndedIterator"
            "advance_back_by"
            advance_back_by.
        Definition nth_back
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.tuple [];
                                            Ty.apply
                                              (Ty.path "core::num::nonzero::NonZero")
                                              []
                                              [ Ty.path "usize" ]
                                          ],
                                        "is_err",
                                        []
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::double_ended::DoubleEndedIterator",
                                              Self,
                                              [],
                                              "advance_back_by",
                                              []
                                            |),
                                            [ M.read (| self |); M.read (| n |) ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      Value.StructTuple "core::option::Option::None" []
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::double_ended::DoubleEndedIterator",
                          Self,
                          [],
                          "next_back",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_nth_back :
          M.IsProvidedMethod
            "core::iter::traits::double_ended::DoubleEndedIterator"
            "nth_back"
            nth_back.
        Definition try_rfold
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          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~ accum := M.copy (| init |) in
                    let~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::double_ended::DoubleEndedIterator",
                                          Self,
                                          [],
                                          "next_back",
                                          []
                                        |),
                                        [ M.read (| self |) ]
                                      |)
                                    |) in
                                  let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let x := M.copy (| γ0_0 |) in
                                  let~ _ :=
                                    M.write (|
                                      accum,
                                      M.read (|
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::try_trait::Try",
                                                R,
                                                [],
                                                "branch",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::function::FnMut",
                                                    F,
                                                    [ Ty.tuple [ B; Ty.associated ] ],
                                                    "call_mut",
                                                    []
                                                  |),
                                                  [
                                                    f;
                                                    Value.Tuple
                                                      [ M.read (| accum |); M.read (| x |) ]
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ0_0 :=
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    γ,
                                                    "core::ops::control_flow::ControlFlow::Break",
                                                    0
                                                  |) in
                                                let residual := M.copy (| γ0_0 |) in
                                                M.alloc (|
                                                  M.never_to_any (|
                                                    M.read (|
                                                      M.return_ (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::FromResidual",
                                                            R,
                                                            [ Ty.associated ],
                                                            "from_residual",
                                                            []
                                                          |),
                                                          [ M.read (| residual |) ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ0_0 :=
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    γ,
                                                    "core::ops::control_flow::ControlFlow::Continue",
                                                    0
                                                  |) in
                                                let val := M.copy (| γ0_0 |) in
                                                val))
                                          ]
                                        |)
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          R,
                          [],
                          "from_output",
                          []
                        |),
                        [ M.read (| accum |) ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_try_rfold :
          M.IsProvidedMethod
            "core::iter::traits::double_ended::DoubleEndedIterator"
            "try_rfold"
            try_rfold.
        Definition rfold (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          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~ accum := M.copy (| init |) in
                let~ _ :=
                  M.loop (|
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::double_ended::DoubleEndedIterator",
                                      Self,
                                      [],
                                      "next_back",
                                      []
                                    |),
                                    [ self ]
                                  |)
                                |) in
                              let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let x := M.copy (| γ0_0 |) in
                              let~ _ :=
                                M.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 (|
                                M.never_to_any (|
                                  M.read (|
                                    let~ _ :=
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  |) in
                accum
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_rfold :
          M.IsProvidedMethod "core::iter::traits::double_ended::DoubleEndedIterator" "rfold" rfold.
        Definition rfind (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::ops::control_flow::ControlFlow")
                    []
                    [ Ty.associated; Ty.tuple [] ],
                  "break_value",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::double_ended::DoubleEndedIterator",
                      Self,
                      [],
                      "try_rfold",
                      [
                        Ty.tuple [];
                        Ty.associated;
                        Ty.apply
                          (Ty.path "core::ops::control_flow::ControlFlow")
                          []
                          [ Ty.associated; Ty.tuple [] ]
                      ]
                    |),
                    [
                      M.read (| self |);
                      Value.Tuple [];
                      M.call_closure (|
                        M.get_associated_function (| Self, "check.rfind", [] |),
                        [ M.read (| predicate |) ]
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_rfind :
          M.IsProvidedMethod "core::iter::traits::double_ended::DoubleEndedIterator" "rfind" rfind.
      End DoubleEndedIterator.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_iter_traits_double_ended_DoubleEndedIterator_I_where_core_marker_Sized_I_for_ref_mut_I.
        Definition Self (I : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ I ].
        
        (*
            fn next_back(&mut self) -> Option<I::Item> {
                ( **self).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.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  I,
                  [],
                  "next_back",
                  []
                |),
                [ M.read (| M.read (| self |) |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                ( **self).advance_back_by(n)
            }
        *)
        Definition advance_back_by
            (I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  I,
                  [],
                  "advance_back_by",
                  []
                |),
                [ M.read (| M.read (| self |) |); M.read (| n |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth_back(&mut self, n: usize) -> Option<I::Item> {
                ( **self).nth_back(n)
            }
        *)
        Definition nth_back (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  I,
                  [],
                  "nth_back",
                  []
                |),
                [ M.read (| M.read (| self |) |); M.read (| n |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn rfold<B, F>(self, init: B, f: F) -> B
            where
                F: FnMut(B, Self::Item) -> B,
            {
                self.spec_rfold(init, f)
            }
        *)
        Definition 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 ], [ 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_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIteratorRefSpec",
                  Ty.apply (Ty.path "&mut") [] [ I ],
                  [],
                  "spec_rfold",
                  [ B; F ]
                |),
                [ M.read (| self |); M.read (| init |); M.read (| f |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_rfold<B, F, R>(&mut self, init: B, f: F) -> R
            where
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                self.spec_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.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIteratorRefSpec",
                  Ty.apply (Ty.path "&mut") [] [ I ],
                  [],
                  "spec_try_rfold",
                  [ B; F; R ]
                |),
                [ M.read (| self |); M.read (| init |); M.read (| f |) ]
              |)))
          | _, _, _ => 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));
              ("advance_back_by", InstanceField.Method (advance_back_by I));
              ("nth_back", InstanceField.Method (nth_back I));
              ("rfold", InstanceField.Method (rfold I));
              ("try_rfold", InstanceField.Method (try_rfold I))
            ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_iter_traits_double_ended_DoubleEndedIterator_I_where_core_marker_Sized_I_for_ref_mut_I.
      
      (* Trait *)
      (* Empty module 'DoubleEndedIteratorRefSpec' *)
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIteratorRefSpec_where_core_iter_traits_double_ended_DoubleEndedIterator_I_where_core_marker_Sized_I_for_ref_mut_I.
        Definition Self (I : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ I ].
        
        (*
            default fn spec_rfold<B, F>(self, init: B, mut f: F) -> B
            where
                F: FnMut(B, Self::Item) -> B,
            {
                let mut accum = init;
                while let Some(x) = self.next_back() {
                    accum = f(accum, x);
                }
                accum
            }
        *)
        Definition spec_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 ], [ 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~ accum := M.copy (| init |) in
                let~ _ :=
                  M.loop (|
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::double_ended::DoubleEndedIterator",
                                      I,
                                      [],
                                      "next_back",
                                      []
                                    |),
                                    [ M.read (| self |) ]
                                  |)
                                |) in
                              let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let x := M.copy (| γ0_0 |) in
                              let~ _ :=
                                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 (|
                                M.never_to_any (|
                                  M.read (|
                                    let~ _ :=
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  |) in
                accum
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            default fn spec_try_rfold<B, F, R>(&mut self, init: B, mut f: F) -> R
            where
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                let mut accum = init;
                while let Some(x) = self.next_back() {
                    accum = f(accum, x)?;
                }
                try { accum }
            }
        *)
        Definition spec_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.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ accum := M.copy (| init |) in
                    let~ _ :=
                      M.loop (|
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::double_ended::DoubleEndedIterator",
                                          Ty.apply (Ty.path "&mut") [] [ I ],
                                          [],
                                          "next_back",
                                          []
                                        |),
                                        [ M.read (| self |) ]
                                      |)
                                    |) in
                                  let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let x := M.copy (| γ0_0 |) in
                                  let~ _ :=
                                    M.write (|
                                      accum,
                                      M.read (|
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::try_trait::Try",
                                                R,
                                                [],
                                                "branch",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::function::FnMut",
                                                    F,
                                                    [ Ty.tuple [ B; Ty.associated ] ],
                                                    "call_mut",
                                                    []
                                                  |),
                                                  [
                                                    f;
                                                    Value.Tuple
                                                      [ M.read (| accum |); M.read (| x |) ]
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ0_0 :=
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    γ,
                                                    "core::ops::control_flow::ControlFlow::Break",
                                                    0
                                                  |) in
                                                let residual := M.copy (| γ0_0 |) in
                                                M.alloc (|
                                                  M.never_to_any (|
                                                    M.read (|
                                                      M.return_ (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::try_trait::FromResidual",
                                                            R,
                                                            [ Ty.associated ],
                                                            "from_residual",
                                                            []
                                                          |),
                                                          [ M.read (| residual |) ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ0_0 :=
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    γ,
                                                    "core::ops::control_flow::ControlFlow::Continue",
                                                    0
                                                  |) in
                                                let val := M.copy (| γ0_0 |) in
                                                val))
                                          ]
                                        |)
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |)))
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          R,
                          [],
                          "from_output",
                          []
                        |),
                        [ M.read (| accum |) ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::double_ended::DoubleEndedIteratorRefSpec"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("spec_rfold", InstanceField.Method (spec_rfold I));
              ("spec_try_rfold", InstanceField.Method (spec_try_rfold I))
            ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIteratorRefSpec_where_core_iter_traits_double_ended_DoubleEndedIterator_I_where_core_marker_Sized_I_for_ref_mut_I.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIteratorRefSpec_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_ref_mut_I.
        Definition Self (I : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ I ].
        
        (*
                fn $fold<AAA, FFF>(mut self, init: AAA, fold: FFF) -> AAA
                where
                    FFF: FnMut(AAA, Self::Item) -> AAA,
                {
                    use crate::ops::NeverShortCircuit;
        
                    self.$try_fold(init, NeverShortCircuit::wrap_mut_2(fold)).0
                }
        *)
        Definition spec_rfold
            (I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ AAA; FFF ], [ 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.SubPointer.get_struct_tuple_field (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::double_ended::DoubleEndedIteratorRefSpec",
                        Ty.apply (Ty.path "&mut") [] [ I ],
                        [],
                        "spec_try_rfold",
                        [
                          AAA;
                          Ty.associated;
                          Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ AAA ]
                        ]
                      |),
                      [
                        self;
                        M.read (| init |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ AAA ],
                            "wrap_mut_2",
                            [ AAA; Ty.associated; FFF ]
                          |),
                          [ M.read (| fold |) ]
                        |)
                      ]
                    |)
                  |),
                  "core::ops::try_trait::NeverShortCircuit",
                  0
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn spec_try_rfold<B, F, R>(&mut self, init: B, f: F) -> R
            where
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                ( **self).try_rfold(init, f)
            }
        *)
        Definition spec_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.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  I,
                  [],
                  "try_rfold",
                  [ B; F; R ]
                |),
                [ M.read (| M.read (| self |) |); M.read (| init |); M.read (| f |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::double_ended::DoubleEndedIteratorRefSpec"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("spec_rfold", InstanceField.Method (spec_rfold I));
              ("spec_try_rfold", InstanceField.Method (spec_try_rfold I))
            ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIteratorRefSpec_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_ref_mut_I.
    End double_ended.
  End traits.
End iter.
