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

Module iter.
  Module sources.
    Module repeat.
      (*
      pub fn repeat<T: Clone>(elt: T) -> Repeat<T> {
          Repeat { element: elt }
      }
      *)
      Definition repeat (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ elt ] =>
          ltac:(M.monadic
            (let elt := M.alloc (| elt |) in
            Value.StructRecord
              "core::iter::sources::repeat::Repeat"
              [ ("element", M.read (| elt |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_repeat : M.IsFunction "core::iter::sources::repeat::repeat" repeat.
      
      (* StructRecord
        {
          name := "Repeat";
          const_params := [];
          ty_params := [ "A" ];
          fields := [ ("element", A) ];
        } *)
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_A_for_core_iter_sources_repeat_Repeat_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat::Repeat") [] [ A ].
        
        (* Clone *)
        Definition clone (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructRecord
                "core::iter::sources::repeat::Repeat"
                [
                  ("element",
                    M.call_closure (|
                      M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::sources::repeat::Repeat",
                          "element"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A : Ty.t),
          M.IsTraitInstance
            "core::clone::Clone"
            (Self A)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method (clone A)) ].
      End Impl_core_clone_Clone_where_core_clone_Clone_A_for_core_iter_sources_repeat_Repeat_A.
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_A_for_core_iter_sources_repeat_Repeat_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat::Repeat") [] [ A ].
        
        (* Debug *)
        Definition fmt (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self A 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 "Repeat" |);
                  M.read (| Value.String "element" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::sources::repeat::Repeat",
                      "element"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A : Ty.t),
          M.IsTraitInstance
            "core::fmt::Debug"
            (Self A)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method (fmt A)) ].
      End Impl_core_fmt_Debug_where_core_fmt_Debug_A_for_core_iter_sources_repeat_Repeat_A.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_Repeat_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat::Repeat") [] [ A ].
        
        (*     type Item = A; *)
        Definition _Item (A : Ty.t) : Ty.t := A.
        
        (*
            fn next(&mut self) -> Option<A> {
                Some(self.element.clone())
            }
        *)
        Definition next (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructTuple
                "core::option::Option::Some"
                [
                  M.call_closure (|
                    M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::sources::repeat::Repeat",
                        "element"
                      |)
                    ]
                  |)
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                (usize::MAX, None)
            }
        *)
        Definition size_hint (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.Tuple
                [
                  M.read (| M.get_constant (| "core::num::MAX" |) |);
                  Value.StructTuple "core::option::Option::None" []
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                // Advancing an infinite iterator of a single element is a no-op.
                let _ = n;
                Ok(())
            }
        *)
        Definition advance_by
            (A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self A 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 (|
                  n,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth(&mut self, n: usize) -> Option<A> {
                let _ = n;
                Some(self.element.clone())
            }
        *)
        Definition nth (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self A 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 (|
                  n,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              M.call_closure (|
                                M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::sources::repeat::Repeat",
                                    "element"
                                  |)
                                ]
                              |)
                            ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn last(self) -> Option<A> {
                loop {}
            }
        *)
        Definition last (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.never_to_any (|
                M.read (| M.loop (| ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) |) |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn count(self) -> usize {
                loop {}
            }
        *)
        Definition count (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.never_to_any (|
                M.read (| M.loop (| ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) |) |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self A)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item A));
              ("next", InstanceField.Method (next A));
              ("size_hint", InstanceField.Method (size_hint A));
              ("advance_by", InstanceField.Method (advance_by A));
              ("nth", InstanceField.Method (nth A));
              ("last", InstanceField.Method (last A));
              ("count", InstanceField.Method (count A))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_Repeat_A.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_Repeat_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat::Repeat") [] [ A ].
        
        (*
            fn next_back(&mut self) -> Option<A> {
                Some(self.element.clone())
            }
        *)
        Definition next_back (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self A in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructTuple
                "core::option::Option::Some"
                [
                  M.call_closure (|
                    M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::sources::repeat::Repeat",
                        "element"
                      |)
                    ]
                  |)
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                // Advancing an infinite iterator of a single element is a no-op.
                let _ = n;
                Ok(())
            }
        *)
        Definition advance_back_by
            (A : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self A 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 (|
                  n,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth_back(&mut self, n: usize) -> Option<A> {
                let _ = n;
                Some(self.element.clone())
            }
        *)
        Definition nth_back (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self A 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 (|
                  n,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              M.call_closure (|
                                M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::sources::repeat::Repeat",
                                    "element"
                                  |)
                                ]
                              |)
                            ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::double_ended::DoubleEndedIterator"
            (Self A)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("next_back", InstanceField.Method (next_back A));
              ("advance_back_by", InstanceField.Method (advance_back_by A));
              ("nth_back", InstanceField.Method (nth_back A))
            ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_Repeat_A.
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_Repeat_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat::Repeat") [] [ A ].
        
        Axiom Implements :
          forall (A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::FusedIterator"
            (Self A)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_FusedIterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_Repeat_A.
      
      Module Impl_core_iter_traits_marker_TrustedLen_where_core_clone_Clone_A_for_core_iter_sources_repeat_Repeat_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat::Repeat") [] [ A ].
        
        Axiom Implements :
          forall (A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::TrustedLen"
            (Self A)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_TrustedLen_where_core_clone_Clone_A_for_core_iter_sources_repeat_Repeat_A.
    End repeat.
  End sources.
End iter.
