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

Module Impl_Tuple_.
  Definition Self : Ty.t := Ty.tuple [].
End Impl_Tuple_.

Module Impl_Tuple_T_.
  Definition Self (T : Ty.t) : Ty.t := Ty.tuple [ T ].
End Impl_Tuple_T_.

Module Impl_TToRet.
  Definition Self (Ret T : Ty.t) : Ty.t := Ty.function [ T ] Ret.
End Impl_TToRet.
