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

(* StructTuple
  {
    name := "LoopA";
    const_params := [];
    ty_params := [];
    fields := [];
  } *)

Module Impl_mutual_loop_LoopA.
  Definition Self : Ty.t := Ty.path "mutual_loop::LoopA".
  
  Parameter new : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  
  Parameter start_loop : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_start_loop : M.IsAssociatedFunction Self "start_loop" start_loop.
End Impl_mutual_loop_LoopA.

(*
Enum LoopB
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Item";
        item := StructRecord [ ("ident", Ty.path "mutual_loop::LoopA") ];
        discriminant := None;
      }
    ];
}
*)

Module Impl_mutual_loop_LoopB.
  Definition Self : Ty.t := Ty.path "mutual_loop::LoopB".
  
  Parameter start_loop : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_start_loop : M.IsAssociatedFunction Self "start_loop" start_loop.
End Impl_mutual_loop_LoopB.

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

Axiom Function_start_loop : M.IsFunction "mutual_loop::start_loop" start_loop.
