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

(* Trait *)
(* Empty module 'PrintInOption' *)

Module Impl_generics_where_clauses_PrintInOption_where_core_fmt_Debug_core_option_Option_T_for_T.
  Definition Self (T : Ty.t) : Ty.t := T.
  
  Parameter print_in_option :
      forall (T : Ty.t),
      (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    forall (T : Ty.t),
    M.IsTraitInstance
      "generics_where_clauses::PrintInOption"
      (Self T)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("print_in_option", InstanceField.Method (print_in_option T)) ].
End Impl_generics_where_clauses_PrintInOption_where_core_fmt_Debug_core_option_Option_T_for_T.

Parameter main : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Axiom Function_main : M.IsFunction "generics_where_clauses::main" main.
