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

(* StructTuple
  {
    name := "Foo";
    const_params := [];
    ty_params := [];
    fields := [ Ty.path "u32" ];
  } *)

Module Impl_example05_Foo.
  Definition Self : Ty.t := Ty.path "example05::Foo".
  
  Parameter plus1 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_plus1 : M.IsAssociatedFunction Self "plus1" plus1.
End Impl_example05_Foo.

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

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