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

Module iter.
  Module adapters.
    Module rev.
      (* StructRecord
        {
          name := "Rev";
          const_params := [];
          ty_params := [ "T" ];
          fields := [ ("iter", T) ];
        } *)
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_iter_adapters_rev_Rev_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::rev::Rev") [] [ T ].
        
        (* Clone *)
        Definition clone (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructRecord
                "core::iter::adapters::rev::Rev"
                [
                  ("iter",
                    M.call_closure (|
                      M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::rev::Rev",
                          "iter"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::clone::Clone"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method (clone T)) ].
      End Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_iter_adapters_rev_Rev_T.
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_iter_adapters_rev_Rev_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::rev::Rev") [] [ T ].
        
        (* Debug *)
        Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T 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_field1_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "Rev" |);
                  M.read (| Value.String "iter" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::rev::Rev",
                      "iter"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::fmt::Debug"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
      End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_iter_adapters_rev_Rev_T.
      
      Module Impl_core_iter_adapters_rev_Rev_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::rev::Rev") [] [ T ].
        
        (*
            pub(in crate::iter) fn new(iter: T) -> Rev<T> {
                Rev { iter }
            }
        *)
        Definition new (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ iter ] =>
            ltac:(M.monadic
              (let iter := M.alloc (| iter |) in
              Value.StructRecord "core::iter::adapters::rev::Rev" [ ("iter", M.read (| iter |)) ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (T : Ty.t),
          M.IsAssociatedFunction (Self T) "new" (new T).
      End Impl_core_iter_adapters_rev_Rev_T.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_rev_Rev_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::rev::Rev") [] [ I ].
        
        (*     type Item = <I as Iterator>::Item; *)
        Definition _Item (I : Ty.t) : Ty.t := Ty.associated.
        
        (*
            fn next(&mut self) -> Option<<I as Iterator>::Item> {
                self.iter.next_back()
            }
        *)
        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.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::rev::Rev",
                    "iter"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                self.iter.size_hint()
            }
        *)
        Definition size_hint (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "size_hint",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::rev::Rev",
                    "iter"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                self.iter.advance_back_by(n)
            }
        *)
        Definition advance_by
            (I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  I,
                  [],
                  "advance_back_by",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::rev::Rev",
                    "iter"
                  |);
                  M.read (| n |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth(&mut self, n: usize) -> Option<<I as Iterator>::Item> {
                self.iter.nth_back(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.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  I,
                  [],
                  "nth_back",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::rev::Rev",
                    "iter"
                  |);
                  M.read (| n |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_fold<B, F, R>(&mut self, init: B, f: F) -> R
            where
                Self: Sized,
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                self.iter.try_rfold(init, 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.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::rev::Rev",
                    "iter"
                  |);
                  M.read (| init |);
                  M.read (| f |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn fold<Acc, F>(self, init: Acc, f: F) -> Acc
            where
                F: FnMut(Acc, Self::Item) -> Acc,
            {
                self.iter.rfold(init, f)
            }
        *)
        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; 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::DoubleEndedIterator",
                  I,
                  [],
                  "rfold",
                  [ Acc; F ]
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::iter::adapters::rev::Rev",
                      "iter"
                    |)
                  |);
                  M.read (| init |);
                  M.read (| f |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn find<P>(&mut self, predicate: P) -> Option<Self::Item>
            where
                P: FnMut(&Self::Item) -> bool,
            {
                self.iter.rfind(predicate)
            }
        *)
        Definition find (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          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_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  I,
                  [],
                  "rfind",
                  [ P ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::rev::Rev",
                    "iter"
                  |);
                  M.read (| predicate |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item I));
              ("next", InstanceField.Method (next I));
              ("size_hint", InstanceField.Method (size_hint I));
              ("advance_by", InstanceField.Method (advance_by I));
              ("nth", InstanceField.Method (nth I));
              ("try_fold", InstanceField.Method (try_fold I));
              ("fold", InstanceField.Method (fold I));
              ("find", InstanceField.Method (find I))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_rev_Rev_I.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_rev_Rev_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::rev::Rev") [] [ I ].
        
        (*
            fn next_back(&mut self) -> Option<<I as Iterator>::Item> {
                self.iter.next()
            }
        *)
        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::iterator::Iterator",
                  I,
                  [],
                  "next",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::rev::Rev",
                    "iter"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                self.iter.advance_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::iterator::Iterator",
                  I,
                  [],
                  "advance_by",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::rev::Rev",
                    "iter"
                  |);
                  M.read (| n |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth_back(&mut self, n: usize) -> Option<<I as Iterator>::Item> {
                self.iter.nth(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::iterator::Iterator", I, [], "nth", [] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::rev::Rev",
                    "iter"
                  |);
                  M.read (| n |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_rfold<B, F, R>(&mut self, init: B, f: F) -> R
            where
                Self: Sized,
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                self.iter.try_fold(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::iterator::Iterator",
                  I,
                  [],
                  "try_fold",
                  [ B; F; R ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::rev::Rev",
                    "iter"
                  |);
                  M.read (| init |);
                  M.read (| f |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn rfold<Acc, F>(self, init: Acc, f: F) -> Acc
            where
                F: FnMut(Acc, Self::Item) -> Acc,
            {
                self.iter.fold(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
          | [], [ Acc; 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::iterator::Iterator",
                  I,
                  [],
                  "fold",
                  [ Acc; F ]
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::iter::adapters::rev::Rev",
                      "iter"
                    |)
                  |);
                  M.read (| init |);
                  M.read (| f |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn rfind<P>(&mut self, predicate: P) -> Option<Self::Item>
            where
                P: FnMut(&Self::Item) -> bool,
            {
                self.iter.find(predicate)
            }
        *)
        Definition rfind (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          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_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "find",
                  [ P ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::rev::Rev",
                    "iter"
                  |);
                  M.read (| predicate |)
                ]
              |)))
          | _, _, _ => 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));
              ("try_rfold", InstanceField.Method (try_rfold I));
              ("rfold", InstanceField.Method (rfold I));
              ("rfind", InstanceField.Method (rfind I))
            ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_rev_Rev_I.
      
      Module Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_iter_traits_exact_size_ExactSizeIterator_I_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_rev_Rev_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::rev::Rev") [] [ I ].
        
        (*
            fn len(&self) -> usize {
                self.iter.len()
            }
        *)
        Definition len (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::exact_size::ExactSizeIterator",
                  I,
                  [],
                  "len",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::rev::Rev",
                    "iter"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn is_empty(&self) -> bool {
                self.iter.is_empty()
            }
        *)
        Definition is_empty (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::exact_size::ExactSizeIterator",
                  I,
                  [],
                  "is_empty",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::rev::Rev",
                    "iter"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::exact_size::ExactSizeIterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("len", InstanceField.Method (len I)); ("is_empty", InstanceField.Method (is_empty I))
            ].
      End Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_iter_traits_exact_size_ExactSizeIterator_I_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_rev_Rev_I.
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_marker_FusedIterator_I_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_rev_Rev_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::rev::Rev") [] [ I ].
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::FusedIterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_marker_FusedIterator_I_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_rev_Rev_I.
      
      Module Impl_core_iter_traits_marker_TrustedLen_where_core_iter_traits_marker_TrustedLen_I_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_rev_Rev_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::rev::Rev") [] [ 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_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_rev_Rev_I.
      
      Module Impl_core_default_Default_where_core_default_Default_I_for_core_iter_adapters_rev_Rev_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::rev::Rev") [] [ I ].
        
        (*
            fn default() -> Self {
                Rev::new(Default::default())
            }
        *)
        Definition default (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::rev::Rev") [] [ I ],
                  "new",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (| "core::default::Default", I, [], "default", [] |),
                    []
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::default::Default"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method (default I)) ].
      End Impl_core_default_Default_where_core_default_Default_I_for_core_iter_adapters_rev_Rev_I.
    End rev.
  End adapters.
End iter.
