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

(* Trait *)
Module ProvidedAndRequired.
  Parameter provided : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom ProvidedMethod_provided :
    M.IsProvidedMethod "provided_method::ProvidedAndRequired" "provided" provided.
End ProvidedAndRequired.

Module Impl_provided_method_ProvidedAndRequired_for_i32.
  Definition Self : Ty.t := Ty.path "i32".
  
  Parameter required : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "provided_method::ProvidedAndRequired"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("required", InstanceField.Method required) ].
End Impl_provided_method_ProvidedAndRequired_for_i32.

Module Impl_provided_method_ProvidedAndRequired_for_u32.
  Definition Self : Ty.t := Ty.path "u32".
  
  Parameter required : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Parameter provided : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "provided_method::ProvidedAndRequired"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [ ("required", InstanceField.Method required); ("provided", InstanceField.Method provided) ].
End Impl_provided_method_ProvidedAndRequired_for_u32.

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

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