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

(*
Enum Food
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "CordonBleu";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "Steak";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "Sushi";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

Module Impl_core_fmt_Debug_for_combinators_and_then_Food.
  Definition Self : Ty.t := Ty.path "combinators_and_then::Food".
  
  Parameter fmt : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::fmt::Debug"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
End Impl_core_fmt_Debug_for_combinators_and_then_Food.

(*
Enum Day
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Monday";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "Tuesday";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "Wednesday";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

Module Impl_core_fmt_Debug_for_combinators_and_then_Day.
  Definition Self : Ty.t := Ty.path "combinators_and_then::Day".
  
  Parameter fmt : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::fmt::Debug"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
End Impl_core_fmt_Debug_for_combinators_and_then_Day.

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

Axiom Function_have_ingredients :
  M.IsFunction "combinators_and_then::have_ingredients" have_ingredients.

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

Axiom Function_have_recipe : M.IsFunction "combinators_and_then::have_recipe" have_recipe.

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

Axiom Function_cookable_v1 : M.IsFunction "combinators_and_then::cookable_v1" cookable_v1.

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

Axiom Function_cookable_v2 : M.IsFunction "combinators_and_then::cookable_v2" cookable_v2.

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

Axiom Function_eat : M.IsFunction "combinators_and_then::eat" eat.

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

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