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

Module underscore.
  (* StructRecord
    {
      name := "Foo";
      const_params := [];
      ty_params := [];
      fields := [ ("test", Ty.path "bool") ];
    } *)
  Module Impl_const_underscore_expression_BarTrait_for_const_underscore_expression_Bar.
    Definition Self : Ty.t := Ty.path "const_underscore_expression::Bar".
    
    Parameter show : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom Implements :
      M.IsTraitInstance
        "const_underscore_expression::BarTrait"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("show", InstanceField.Method show) ].
  End Impl_const_underscore_expression_BarTrait_for_const_underscore_expression_Bar.
End underscore.

(* StructRecord
  {
    name := "Bar";
    const_params := [];
    ty_params := [];
    fields := [ ("test", Ty.path "alloc::string::String") ];
  } *)

(* Trait *)
(* Empty module 'BarTrait' *)

