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

Module my.
  (* StructRecord
    {
      name := "OpenBox";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ ("contents", T) ];
    } *)
  
  (* StructRecord
    {
      name := "ClosedBox";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ ("contents", T) ];
    } *)
  
  Module Impl_struct_visibility_my_ClosedBox_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "struct_visibility::my::ClosedBox") [] [ T ].
    
    Parameter new : forall (T : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
    
    Axiom AssociatedFunction_new : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "new" (new T).
  End Impl_struct_visibility_my_ClosedBox_T.
End my.

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

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