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

Module future.
  Module into_future.
    (* Trait *)
    (* Empty module 'IntoFuture' *)
    
    Module Impl_core_future_into_future_IntoFuture_where_core_future_future_Future_F_for_F.
      Definition Self (F : Ty.t) : Ty.t := F.
      
      (*     type Output = F::Output; *)
      Definition _Output (F : Ty.t) : Ty.t := Ty.associated.
      
      (*     type IntoFuture = F; *)
      Definition _IntoFuture (F : Ty.t) : Ty.t := F.
      
      (*
          fn into_future(self) -> Self::IntoFuture {
              self
          }
      *)
      Definition into_future (F : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self F in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| self |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (F : Ty.t),
        M.IsTraitInstance
          "core::future::into_future::IntoFuture"
          (Self F)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output F));
            ("IntoFuture", InstanceField.Ty (_IntoFuture F));
            ("into_future", InstanceField.Method (into_future F))
          ].
    End Impl_core_future_into_future_IntoFuture_where_core_future_future_Future_F_for_F.
  End into_future.
End future.
