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

(*
Enum VeryVerboseEnumOfThingsToDoWithNumbers
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Add";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "Subtract";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

Module Impl_enums_type_aliases_v2_VeryVerboseEnumOfThingsToDoWithNumbers.
  Definition Self : Ty.t := Ty.path "enums_type_aliases_v2::VeryVerboseEnumOfThingsToDoWithNumbers".
  
  (*
      fn run(&self, x: i32, y: i32) -> i32 {
          match self {
              Self::Add => x + y,
              Self::Subtract => x - y,
          }
      }
  *)
  Definition run (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; x; y ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let x := M.alloc (| x |) in
        let y := M.alloc (| y |) in
        M.read (|
          M.match_operator (|
            self,
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let _ :=
                    M.is_struct_tuple (|
                      γ,
                      "enums_type_aliases_v2::VeryVerboseEnumOfThingsToDoWithNumbers::Add"
                    |) in
                  M.alloc (| BinOp.Wrap.add (| M.read (| x |), M.read (| y |) |) |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let _ :=
                    M.is_struct_tuple (|
                      γ,
                      "enums_type_aliases_v2::VeryVerboseEnumOfThingsToDoWithNumbers::Subtract"
                    |) in
                  M.alloc (| BinOp.Wrap.sub (| M.read (| x |), M.read (| y |) |) |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_run : M.IsAssociatedFunction Self "run" run.
End Impl_enums_type_aliases_v2_VeryVerboseEnumOfThingsToDoWithNumbers.
