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

Module iter.
  Module traits.
    Module unchecked_iterator.
      (* Trait *)
      Module UncheckedIterator.
        Definition next_unchecked
            (Self : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ opt :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Self,
                        [],
                        "next",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ],
                      "unwrap_unchecked",
                      []
                    |),
                    [ M.read (| opt |) ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom ProvidedMethod_next_unchecked :
          M.IsProvidedMethod
            "core::iter::traits::unchecked_iterator::UncheckedIterator"
            "next_unchecked"
            next_unchecked.
      End UncheckedIterator.
    End unchecked_iterator.
  End traits.
End iter.
