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

Module iter.
  Module sources.
    Module once.
      (*
      pub fn once<T>(value: T) -> Once<T> {
          Once { inner: Some(value).into_iter() }
      }
      *)
      Definition once (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T ], [ value ] =>
          ltac:(M.monadic
            (let value := M.alloc (| value |) in
            Value.StructRecord
              "core::iter::sources::once::Once"
              [
                ("inner",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::collect::IntoIterator",
                      Ty.apply (Ty.path "core::option::Option") [] [ T ],
                      [],
                      "into_iter",
                      []
                    |),
                    [ Value.StructTuple "core::option::Option::Some" [ M.read (| value |) ] ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_once : M.IsFunction "core::iter::sources::once::once" once.
      
      (* StructRecord
        {
          name := "Once";
          const_params := [];
          ty_params := [ "T" ];
          fields := [ ("inner", Ty.apply (Ty.path "core::option::IntoIter") [] [ T ]) ];
        } *)
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_iter_sources_once_Once_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once::Once") [] [ 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::sources::once::Once"
                [
                  ("inner",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply (Ty.path "core::option::IntoIter") [] [ T ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::sources::once::Once",
                          "inner"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => 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_sources_once_Once_T.
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_iter_sources_once_Once_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once::Once") [] [ 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 "Once" |);
                  M.read (| Value.String "inner" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::sources::once::Once",
                      "inner"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => 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_sources_once_Once_T.
      
      Module Impl_core_iter_traits_iterator_Iterator_for_core_iter_sources_once_Once_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once::Once") [] [ T ].
        
        (*     type Item = T; *)
        Definition _Item (T : Ty.t) : Ty.t := T.
        
        (*
            fn next(&mut self) -> Option<T> {
                self.inner.next()
            }
        *)
        Definition next (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
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply (Ty.path "core::option::IntoIter") [] [ T ],
                  [],
                  "next",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::sources::once::Once",
                    "inner"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                self.inner.size_hint()
            }
        *)
        Definition size_hint (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
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply (Ty.path "core::option::IntoIter") [] [ T ],
                  [],
                  "size_hint",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::sources::once::Once",
                    "inner"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item T));
              ("next", InstanceField.Method (next T));
              ("size_hint", InstanceField.Method (size_hint T))
            ].
      End Impl_core_iter_traits_iterator_Iterator_for_core_iter_sources_once_Once_T.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_iter_sources_once_Once_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once::Once") [] [ T ].
        
        (*
            fn next_back(&mut self) -> Option<T> {
                self.inner.next_back()
            }
        *)
        Definition next_back (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
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  Ty.apply (Ty.path "core::option::IntoIter") [] [ T ],
                  [],
                  "next_back",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::sources::once::Once",
                    "inner"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::double_ended::DoubleEndedIterator"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("next_back", InstanceField.Method (next_back T)) ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_iter_sources_once_Once_T.
      
      Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_iter_sources_once_Once_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once::Once") [] [ T ].
        
        (*
            fn len(&self) -> usize {
                self.inner.len()
            }
        *)
        Definition len (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
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::exact_size::ExactSizeIterator",
                  Ty.apply (Ty.path "core::option::IntoIter") [] [ T ],
                  [],
                  "len",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::sources::once::Once",
                    "inner"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::exact_size::ExactSizeIterator"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("len", InstanceField.Method (len T)) ].
      End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_iter_sources_once_Once_T.
      
      Module Impl_core_iter_traits_marker_TrustedLen_for_core_iter_sources_once_Once_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once::Once") [] [ T ].
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::TrustedLen"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_TrustedLen_for_core_iter_sources_once_Once_T.
      
      Module Impl_core_iter_traits_marker_FusedIterator_for_core_iter_sources_once_Once_T.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::sources::once::Once") [] [ T ].
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::FusedIterator"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_FusedIterator_for_core_iter_sources_once_Once_T.
    End once.
  End sources.
End iter.
