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

Module iter.
  Module sources.
    Module repeat_n.
      (*
      pub fn repeat_n<T: Clone>(element: T, count: usize) -> RepeatN<T> {
          let element = if count == 0 {
              // `element` gets dropped eagerly.
              MaybeUninit::uninit()
          } else {
              MaybeUninit::new(element)
          };
      
          RepeatN { element, count }
      }
      *)
      Definition repeat_n (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ element; count ] =>
          ltac:(M.monadic
            (let element := M.alloc (| element |) in
            let count := M.alloc (| count |) in
            M.read (|
              let~ element :=
                M.copy (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.eq (| M.read (| count |), Value.Integer IntegerKind.Usize 0 |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                                "uninit",
                                []
                              |),
                              []
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                                "new",
                                []
                              |),
                              [ M.read (| element |) ]
                            |)
                          |)))
                    ]
                  |)
                |) in
              M.alloc (|
                Value.StructRecord
                  "core::iter::sources::repeat_n::RepeatN"
                  [ ("element", M.read (| element |)); ("count", M.read (| count |)) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_repeat_n : M.IsFunction "core::iter::sources::repeat_n::repeat_n" repeat_n.
      
      (* StructRecord
        {
          name := "RepeatN";
          const_params := [];
          ty_params := [ "A" ];
          fields :=
            [
              ("count", Ty.path "usize");
              ("element", Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ A ])
            ];
        } *)
      
      Module Impl_core_iter_sources_repeat_n_RepeatN_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ].
        
        (*
            fn element_ref(&self) -> Option<&A> {
                if self.count > 0 {
                    // SAFETY: The count is non-zero, so it must be initialized.
                    Some(unsafe { self.element.assume_init_ref() })
                } else {
                    None
                }
            }
        *)
        Definition element_ref
            (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.read (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.gt (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::sources::repeat_n::RepeatN",
                                    "count"
                                  |)
                                |),
                                Value.Integer IntegerKind.Usize 0
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                    []
                                    [ A ],
                                  "assume_init_ref",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::sources::repeat_n::RepeatN",
                                    "element"
                                  |)
                                ]
                              |)
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_element_ref :
          forall (A : Ty.t),
          M.IsAssociatedFunction (Self A) "element_ref" (element_ref A).
        
        (*
            fn take_element(&mut self) -> Option<A> {
                if self.count > 0 {
                    self.count = 0;
                    let element = mem::replace(&mut self.element, MaybeUninit::uninit());
                    // SAFETY: We just set count to zero so it won't be dropped again,
                    // and it used to be non-zero so it hasn't already been dropped.
                    unsafe { Some(element.assume_init()) }
                } else {
                    None
                }
            }
        *)
        Definition take_element
            (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.read (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.gt (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::sources::repeat_n::RepeatN",
                                    "count"
                                  |)
                                |),
                                Value.Integer IntegerKind.Usize 0
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::iter::sources::repeat_n::RepeatN",
                              "count"
                            |),
                            Value.Integer IntegerKind.Usize 0
                          |) in
                        let~ element :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (|
                                "core::mem::replace",
                                [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ A ]
                                ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::iter::sources::repeat_n::RepeatN",
                                  "element"
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                      []
                                      [ A ],
                                    "uninit",
                                    []
                                  |),
                                  []
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                    []
                                    [ A ],
                                  "assume_init",
                                  []
                                |),
                                [ M.read (| element |) ]
                              |)
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_take_element :
          forall (A : Ty.t),
          M.IsAssociatedFunction (Self A) "take_element" (take_element A).
      End Impl_core_iter_sources_repeat_n_RepeatN_A.
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_A_for_core_iter_sources_repeat_n_RepeatN_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ].
        
        (*
            fn clone(&self) -> RepeatN<A> {
                RepeatN {
                    count: self.count,
                    element: self.element_ref().cloned().map_or_else(MaybeUninit::uninit, MaybeUninit::new),
                }
            }
        *)
        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_n::RepeatN"
                [
                  ("count",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::sources::repeat_n::RepeatN",
                        "count"
                      |)
                    |));
                  ("element",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::option::Option") [] [ A ],
                        "map_or_else",
                        [
                          Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ A ];
                          Ty.function
                            []
                            (Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ A ]);
                          Ty.function
                            [ A ]
                            (Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ A ])
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.apply (Ty.path "&") [] [ A ] ],
                            "cloned",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::iter::sources::repeat_n::RepeatN")
                                  []
                                  [ A ],
                                "element_ref",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          ]
                        |);
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ A ],
                          "uninit",
                          []
                        |);
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ A ],
                          "new",
                          []
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => 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_n_RepeatN_A.
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_A_for_core_iter_sources_repeat_n_RepeatN_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ].
        
        (*
            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                f.debug_struct("RepeatN")
                    .field("count", &self.count)
                    .field("element", &self.element_ref())
                    .finish()
            }
        *)
        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::builders::DebugStruct",
                  "finish",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::builders::DebugStruct",
                      "field",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::builders::DebugStruct",
                          "field",
                          []
                        |),
                        [
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Formatter",
                                "debug_struct",
                                []
                              |),
                              [ M.read (| f |); M.read (| Value.String "RepeatN" |) ]
                            |)
                          |);
                          M.read (| Value.String "count" |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::iter::sources::repeat_n::RepeatN",
                            "count"
                          |)
                        ]
                      |);
                      M.read (| Value.String "element" |);
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ],
                            "element_ref",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => 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_n_RepeatN_A.
      
      Module Impl_core_ops_drop_Drop_for_core_iter_sources_repeat_n_RepeatN_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ].
        
        (*
            fn drop(&mut self) {
                self.take_element();
            }
        *)
        Definition drop (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.read (|
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ],
                        "take_element",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A : Ty.t),
          M.IsTraitInstance
            "core::ops::drop::Drop"
            (Self A)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("drop", InstanceField.Method (drop A)) ].
      End Impl_core_ops_drop_Drop_for_core_iter_sources_repeat_n_RepeatN_A.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_n_RepeatN_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ].
        
        (*     type Item = A; *)
        Definition _Item (A : Ty.t) : Ty.t := A.
        
        (*
            fn next(&mut self) -> Option<A> {
                if self.count > 0 {
                    // SAFETY: Just checked it's not empty
                    unsafe { Some(self.next_unchecked()) }
                } else {
                    None
                }
            }
        *)
        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
              M.read (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.gt (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::sources::repeat_n::RepeatN",
                                    "count"
                                  |)
                                |),
                                Value.Integer IntegerKind.Usize 0
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::unchecked_iterator::UncheckedIterator",
                                  Ty.apply
                                    (Ty.path "core::iter::sources::repeat_n::RepeatN")
                                    []
                                    [ A ],
                                  [],
                                  "next_unchecked",
                                  []
                                |),
                                [ M.read (| self |) ]
                              |)
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                let len = self.len();
                (len, Some(len))
            }
        *)
        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
              M.read (|
                let~ len :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::exact_size::ExactSizeIterator",
                        Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ],
                        [],
                        "len",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                M.alloc (|
                  Value.Tuple
                    [
                      M.read (| len |);
                      Value.StructTuple "core::option::Option::Some" [ M.read (| len |) ]
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_by(&mut self, skip: usize) -> Result<(), NonZero<usize>> {
                let len = self.count;
        
                if skip >= len {
                    self.take_element();
                }
        
                if skip > len {
                    // SAFETY: we just checked that the difference is positive
                    Err(unsafe { NonZero::new_unchecked(skip - len) })
                } else {
                    self.count = len - skip;
                    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; skip ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let skip := M.alloc (| skip |) in
              M.read (|
                let~ len :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::sources::repeat_n::RepeatN",
                      "count"
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (| BinOp.ge (| M.read (| skip |), M.read (| len |) |) |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::iter::sources::repeat_n::RepeatN")
                                    []
                                    [ A ],
                                  "take_element",
                                  []
                                |),
                                [ M.read (| self |) ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (| BinOp.gt (| M.read (| skip |), M.read (| len |) |) |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          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 (| skip |), M.read (| len |) |) ]
                              |)
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::iter::sources::repeat_n::RepeatN",
                              "count"
                            |),
                            BinOp.Wrap.sub (| M.read (| len |), M.read (| skip |) |)
                          |) in
                        M.alloc (|
                          Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn last(mut self) -> Option<A> {
                self.take_element()
            }
        *)
        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.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ],
                  "take_element",
                  []
                |),
                [ self ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn count(self) -> usize {
                self.len()
            }
        *)
        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.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::exact_size::ExactSizeIterator",
                  Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ],
                  [],
                  "len",
                  []
                |),
                [ self ]
              |)))
          | _, _, _ => 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));
              ("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_n_RepeatN_A.
      
      Module Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_n_RepeatN_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ].
        
        (*
            fn len(&self) -> usize {
                self.count
            }
        *)
        Definition len (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.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::iter::sources::repeat_n::RepeatN",
                  "count"
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::exact_size::ExactSizeIterator"
            (Self A)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("len", InstanceField.Method (len A)) ].
      End Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_n_RepeatN_A.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_n_RepeatN_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ].
        
        (*
            fn next_back(&mut self) -> Option<A> {
                self.next()
            }
        *)
        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
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ],
                  [],
                  "next",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                self.advance_by(n)
            }
        *)
        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.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ],
                  [],
                  "advance_by",
                  []
                |),
                [ M.read (| self |); M.read (| n |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth_back(&mut self, n: usize) -> Option<A> {
                self.nth(n)
            }
        *)
        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.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ],
                  [],
                  "nth",
                  []
                |),
                [ M.read (| self |); M.read (| n |) ]
              |)))
          | _, _, _ => 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_n_RepeatN_A.
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_n_RepeatN_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ 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_n_RepeatN_A.
      
      Module Impl_core_iter_traits_marker_TrustedLen_where_core_clone_Clone_A_for_core_iter_sources_repeat_n_RepeatN_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ 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_n_RepeatN_A.
      
      Module Impl_core_iter_traits_unchecked_iterator_UncheckedIterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_n_RepeatN_A.
        Definition Self (A : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ A ].
        
        (*
            unsafe fn next_unchecked(&mut self) -> Self::Item {
                // SAFETY: The caller promised the iterator isn't empty
                self.count = unsafe { self.count.unchecked_sub(1) };
                if self.count == 0 {
                    // SAFETY: the check above ensured that the count used to be non-zero,
                    // so element hasn't been dropped yet, and we just lowered the count to
                    // zero so it won't be dropped later, and thus it's okay to take it here.
                    unsafe { mem::replace(&mut self.element, MaybeUninit::uninit()).assume_init() }
                } else {
                    // SAFETY: the count is non-zero, so it must have not been dropped yet.
                    let element = unsafe { self.element.assume_init_ref() };
                    A::clone(element)
                }
            }
        *)
        Definition next_unchecked
            (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.read (|
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::sources::repeat_n::RepeatN",
                      "count"
                    |),
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "usize", "unchecked_sub", [] |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::iter::sources::repeat_n::RepeatN",
                            "count"
                          |)
                        |);
                        Value.Integer IntegerKind.Usize 1
                      ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::sources::repeat_n::RepeatN",
                                    "count"
                                  |)
                                |),
                                Value.Integer IntegerKind.Usize 0
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ A ],
                              "assume_init",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_function (|
                                  "core::mem::replace",
                                  [
                                    Ty.apply
                                      (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                      []
                                      [ A ]
                                  ]
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::sources::repeat_n::RepeatN",
                                    "element"
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                        []
                                        [ A ],
                                      "uninit",
                                      []
                                    |),
                                    []
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ element :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ A ],
                                "assume_init_ref",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::iter::sources::repeat_n::RepeatN",
                                  "element"
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                            [ M.read (| element |) ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (A : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::unchecked_iterator::UncheckedIterator"
            (Self A)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("next_unchecked", InstanceField.Method (next_unchecked A)) ].
      End Impl_core_iter_traits_unchecked_iterator_UncheckedIterator_where_core_clone_Clone_A_for_core_iter_sources_repeat_n_RepeatN_A.
    End repeat_n.
  End sources.
End iter.
