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

Module ops.
  Module coroutine.
    (*
    Enum CoroutineState
    {
      const_params := [];
      ty_params := [ "Y"; "R" ];
      variants :=
        [
          {
            name := "Yielded";
            item := StructTuple [ Y ];
            discriminant := None;
          };
          {
            name := "Complete";
            item := StructTuple [ R ];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_clone_Clone_where_core_clone_Clone_Y_where_core_clone_Clone_R_for_core_ops_coroutine_CoroutineState_Y_R.
      Definition Self (Y R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ].
      
      (* Clone *)
      Definition clone (Y R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self Y R in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::coroutine::CoroutineState::Yielded",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::coroutine::CoroutineState::Yielded"
                          [
                            M.call_closure (|
                              M.get_trait_method (| "core::clone::Clone", Y, [], "clone", [] |),
                              [ M.read (| __self_0 |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::coroutine::CoroutineState::Complete",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::coroutine::CoroutineState::Complete"
                          [
                            M.call_closure (|
                              M.get_trait_method (| "core::clone::Clone", R, [], "clone", [] |),
                              [ M.read (| __self_0 |) ]
                            |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (Y R : Ty.t),
        M.IsTraitInstance
          "core::clone::Clone"
          (Self Y R)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method (clone Y R)) ].
    End Impl_core_clone_Clone_where_core_clone_Clone_Y_where_core_clone_Clone_R_for_core_ops_coroutine_CoroutineState_Y_R.
    
    Module Impl_core_marker_Copy_where_core_marker_Copy_Y_where_core_marker_Copy_R_for_core_ops_coroutine_CoroutineState_Y_R.
      Definition Self (Y R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ].
      
      Axiom Implements :
        forall (Y R : Ty.t),
        M.IsTraitInstance
          "core::marker::Copy"
          (Self Y R)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_where_core_marker_Copy_Y_where_core_marker_Copy_R_for_core_ops_coroutine_CoroutineState_Y_R.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_ops_coroutine_CoroutineState_Y_R.
      Definition Self (Y R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ].
      
      Axiom Implements :
        forall (Y R : Ty.t),
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          (Self Y R)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_ops_coroutine_CoroutineState_Y_R.
    
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_Y_where_core_cmp_PartialEq_R_for_core_ops_coroutine_CoroutineState_Y_R.
      Definition Self (Y R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ].
      
      (* PartialEq *)
      Definition eq (Y R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self Y R in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ] ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ] ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (|
                LogicalOp.and (|
                  BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |),
                  ltac:(M.monadic
                    (M.read (|
                      M.match_operator (|
                        M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                              let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                              let γ0_0 := M.read (| γ0_0 |) in
                              let γ2_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_0,
                                  "core::ops::coroutine::CoroutineState::Yielded",
                                  0
                                |) in
                              let __self_0 := M.alloc (| γ2_0 |) in
                              let γ0_1 := M.read (| γ0_1 |) in
                              let γ2_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_1,
                                  "core::ops::coroutine::CoroutineState::Yielded",
                                  0
                                |) in
                              let __arg1_0 := M.alloc (| γ2_0 |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.apply (Ty.path "&") [] [ Y ],
                                    [ Ty.apply (Ty.path "&") [] [ Y ] ],
                                    "eq",
                                    []
                                  |),
                                  [ __self_0; __arg1_0 ]
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                              let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                              let γ0_0 := M.read (| γ0_0 |) in
                              let γ2_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_0,
                                  "core::ops::coroutine::CoroutineState::Complete",
                                  0
                                |) in
                              let __self_0 := M.alloc (| γ2_0 |) in
                              let γ0_1 := M.read (| γ0_1 |) in
                              let γ2_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_1,
                                  "core::ops::coroutine::CoroutineState::Complete",
                                  0
                                |) in
                              let __arg1_0 := M.alloc (| γ2_0 |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.apply (Ty.path "&") [] [ R ],
                                    [ Ty.apply (Ty.path "&") [] [ R ] ],
                                    "eq",
                                    []
                                  |),
                                  [ __self_0; __arg1_0 ]
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (|
                                M.never_to_any (|
                                  M.call_closure (|
                                    M.get_function (| "core::intrinsics::unreachable", [] |),
                                    []
                                  |)
                                |)
                              |)))
                        ]
                      |)
                    |)))
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (Y R : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self Y R)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method (eq Y R)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_Y_where_core_cmp_PartialEq_R_for_core_ops_coroutine_CoroutineState_Y_R.
    
    Module Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_Y_where_core_cmp_PartialOrd_R_for_core_ops_coroutine_CoroutineState_Y_R.
      Definition Self (Y R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ].
      
      (* PartialOrd *)
      Definition partial_cmp
          (Y R : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self Y R in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ] ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ] ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.match_operator (|
                M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let γ0_0 := M.read (| γ0_0 |) in
                      let γ2_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ0_0,
                          "core::ops::coroutine::CoroutineState::Yielded",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ2_0 |) in
                      let γ0_1 := M.read (| γ0_1 |) in
                      let γ2_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ0_1,
                          "core::ops::coroutine::CoroutineState::Yielded",
                          0
                        |) in
                      let __arg1_0 := M.alloc (| γ2_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialOrd",
                            Y,
                            [ Y ],
                            "partial_cmp",
                            []
                          |),
                          [ M.read (| __self_0 |); M.read (| __arg1_0 |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let γ0_0 := M.read (| γ0_0 |) in
                      let γ2_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ0_0,
                          "core::ops::coroutine::CoroutineState::Complete",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ2_0 |) in
                      let γ0_1 := M.read (| γ0_1 |) in
                      let γ2_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ0_1,
                          "core::ops::coroutine::CoroutineState::Complete",
                          0
                        |) in
                      let __arg1_0 := M.alloc (| γ2_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialOrd",
                            R,
                            [ R ],
                            "partial_cmp",
                            []
                          |),
                          [ M.read (| __self_0 |); M.read (| __arg1_0 |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialOrd",
                            Ty.path "isize",
                            [ Ty.path "isize" ],
                            "partial_cmp",
                            []
                          |),
                          [ __self_discr; __arg1_discr ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (Y R : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          (Self Y R)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_cmp", InstanceField.Method (partial_cmp Y R)) ].
    End Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_Y_where_core_cmp_PartialOrd_R_for_core_ops_coroutine_CoroutineState_Y_R.
    
    Module Impl_core_cmp_Eq_where_core_cmp_Eq_Y_where_core_cmp_Eq_R_for_core_ops_coroutine_CoroutineState_Y_R.
      Definition Self (Y R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ].
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (Y R : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self Y R in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        Value.DeclaredButUndefined,
                        [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (Y R : Ty.t),
        M.IsTraitInstance
          "core::cmp::Eq"
          (Self Y R)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method (assert_receiver_is_total_eq Y R))
          ].
    End Impl_core_cmp_Eq_where_core_cmp_Eq_Y_where_core_cmp_Eq_R_for_core_ops_coroutine_CoroutineState_Y_R.
    
    Module Impl_core_cmp_Ord_where_core_cmp_Ord_Y_where_core_cmp_Ord_R_for_core_ops_coroutine_CoroutineState_Y_R.
      Definition Self (Y R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ].
      
      (* Ord *)
      Definition cmp (Y R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self Y R in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ] ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ] ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (| "core::cmp::Ord", Ty.path "isize", [], "cmp", [] |),
                    [ __self_discr; __arg1_discr ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                      M.match_operator (|
                        M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                              let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                              let γ0_0 := M.read (| γ0_0 |) in
                              let γ2_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_0,
                                  "core::ops::coroutine::CoroutineState::Yielded",
                                  0
                                |) in
                              let __self_0 := M.alloc (| γ2_0 |) in
                              let γ0_1 := M.read (| γ0_1 |) in
                              let γ2_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_1,
                                  "core::ops::coroutine::CoroutineState::Yielded",
                                  0
                                |) in
                              let __arg1_0 := M.alloc (| γ2_0 |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (| "core::cmp::Ord", Y, [], "cmp", [] |),
                                  [ M.read (| __self_0 |); M.read (| __arg1_0 |) ]
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                              let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                              let γ0_0 := M.read (| γ0_0 |) in
                              let γ2_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_0,
                                  "core::ops::coroutine::CoroutineState::Complete",
                                  0
                                |) in
                              let __self_0 := M.alloc (| γ2_0 |) in
                              let γ0_1 := M.read (| γ0_1 |) in
                              let γ2_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ0_1,
                                  "core::ops::coroutine::CoroutineState::Complete",
                                  0
                                |) in
                              let __arg1_0 := M.alloc (| γ2_0 |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (| "core::cmp::Ord", R, [], "cmp", [] |),
                                  [ M.read (| __self_0 |); M.read (| __arg1_0 |) ]
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (|
                                M.never_to_any (|
                                  M.call_closure (|
                                    M.get_function (| "core::intrinsics::unreachable", [] |),
                                    []
                                  |)
                                |)
                              |)))
                        ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let cmp := M.copy (| γ |) in
                      cmp))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (Y R : Ty.t),
        M.IsTraitInstance
          "core::cmp::Ord"
          (Self Y R)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method (cmp Y R)) ].
    End Impl_core_cmp_Ord_where_core_cmp_Ord_Y_where_core_cmp_Ord_R_for_core_ops_coroutine_CoroutineState_Y_R.
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_Y_where_core_fmt_Debug_R_for_core_ops_coroutine_CoroutineState_Y_R.
      Definition Self (Y R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ].
      
      (* Debug *)
      Definition fmt (Y R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self Y R in
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::coroutine::CoroutineState::Yielded",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "debug_tuple_field1_finish",
                            []
                          |),
                          [ M.read (| f |); M.read (| Value.String "Yielded" |); __self_0 ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::coroutine::CoroutineState::Complete",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "debug_tuple_field1_finish",
                            []
                          |),
                          [ M.read (| f |); M.read (| Value.String "Complete" |); __self_0 ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (Y R : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self Y R)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt Y R)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_Y_where_core_fmt_Debug_R_for_core_ops_coroutine_CoroutineState_Y_R.
    
    Module Impl_core_hash_Hash_where_core_hash_Hash_Y_where_core_hash_Hash_R_for_core_ops_coroutine_CoroutineState_Y_R.
      Definition Self (Y R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ].
      
      (* Hash *)
      Definition hash (Y R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self Y R in
        match ε, τ, α with
        | [], [ __H ], [ self; state ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let state := M.alloc (| state |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.apply (Ty.path "core::ops::coroutine::CoroutineState") [] [ Y; R ] ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::hash::Hash",
                      Ty.path "isize",
                      [],
                      "hash",
                      [ __H ]
                    |),
                    [ __self_discr; M.read (| state |) ]
                  |)
                |) in
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::coroutine::CoroutineState::Yielded",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (| "core::hash::Hash", Y, [], "hash", [ __H ] |),
                          [ M.read (| __self_0 |); M.read (| state |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::coroutine::CoroutineState::Complete",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (| "core::hash::Hash", R, [], "hash", [ __H ] |),
                          [ M.read (| __self_0 |); M.read (| state |) ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (Y R : Ty.t),
        M.IsTraitInstance
          "core::hash::Hash"
          (Self Y R)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("hash", InstanceField.Method (hash Y R)) ].
    End Impl_core_hash_Hash_where_core_hash_Hash_Y_where_core_hash_Hash_R_for_core_ops_coroutine_CoroutineState_Y_R.
    
    (* Trait *)
    (* Empty module 'Coroutine' *)
    
    Module Impl_core_ops_coroutine_Coroutine_where_core_marker_Sized_G_where_core_ops_coroutine_Coroutine_G_R_R_for_core_pin_Pin_ref_mut_G.
      Definition Self (G R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::pin::Pin") [] [ Ty.apply (Ty.path "&mut") [] [ G ] ].
      
      (*     type Yield = G::Yield; *)
      Definition _Yield (G R : Ty.t) : Ty.t := Ty.associated.
      
      (*     type Return = G::Return; *)
      Definition _Return (G R : Ty.t) : Ty.t := Ty.associated.
      
      (*
          fn resume(mut self: Pin<&mut Self>, arg: R) -> CoroutineState<Self::Yield, Self::Return> {
              G::resume(( *self).as_mut(), arg)
          }
      *)
      Definition resume (G R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self G R in
        match ε, τ, α with
        | [], [], [ self; arg ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let arg := M.alloc (| arg |) in
            M.call_closure (|
              M.get_trait_method (| "core::ops::coroutine::Coroutine", G, [ R ], "resume", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::pin::Pin") [] [ Ty.apply (Ty.path "&mut") [] [ G ] ],
                    "as_mut",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::DerefMut",
                        Ty.apply
                          (Ty.path "core::pin::Pin")
                          []
                          [
                            Ty.apply
                              (Ty.path "&mut")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::pin::Pin")
                                  []
                                  [ Ty.apply (Ty.path "&mut") [] [ G ] ]
                              ]
                          ],
                        [],
                        "deref_mut",
                        []
                      |),
                      [ self ]
                    |)
                  ]
                |);
                M.read (| arg |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (G R : Ty.t),
        M.IsTraitInstance
          "core::ops::coroutine::Coroutine"
          (Self G R)
          (* Trait polymorphic types *) [ (* R *) R ]
          (* Instance *)
          [
            ("Yield", InstanceField.Ty (_Yield G R));
            ("Return", InstanceField.Ty (_Return G R));
            ("resume", InstanceField.Method (resume G R))
          ].
    End Impl_core_ops_coroutine_Coroutine_where_core_marker_Sized_G_where_core_ops_coroutine_Coroutine_G_R_R_for_core_pin_Pin_ref_mut_G.
    
    Module Impl_core_ops_coroutine_Coroutine_where_core_marker_Sized_G_where_core_ops_coroutine_Coroutine_G_R_where_core_marker_Unpin_G_R_for_ref_mut_G.
      Definition Self (G R : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ G ].
      
      (*     type Yield = G::Yield; *)
      Definition _Yield (G R : Ty.t) : Ty.t := Ty.associated.
      
      (*     type Return = G::Return; *)
      Definition _Return (G R : Ty.t) : Ty.t := Ty.associated.
      
      (*
          fn resume(mut self: Pin<&mut Self>, arg: R) -> CoroutineState<Self::Yield, Self::Return> {
              G::resume(Pin::new(&mut *self), arg)
          }
      *)
      Definition resume (G R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self G R in
        match ε, τ, α with
        | [], [], [ self; arg ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let arg := M.alloc (| arg |) in
            M.call_closure (|
              M.get_trait_method (| "core::ops::coroutine::Coroutine", G, [ R ], "resume", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::pin::Pin") [] [ Ty.apply (Ty.path "&mut") [] [ G ] ],
                    "new",
                    []
                  |),
                  [
                    M.read (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::deref::DerefMut",
                          Ty.apply
                            (Ty.path "core::pin::Pin")
                            []
                            [ Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "&mut") [] [ G ] ] ],
                          [],
                          "deref_mut",
                          []
                        |),
                        [ self ]
                      |)
                    |)
                  ]
                |);
                M.read (| arg |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (G R : Ty.t),
        M.IsTraitInstance
          "core::ops::coroutine::Coroutine"
          (Self G R)
          (* Trait polymorphic types *) [ (* R *) R ]
          (* Instance *)
          [
            ("Yield", InstanceField.Ty (_Yield G R));
            ("Return", InstanceField.Ty (_Return G R));
            ("resume", InstanceField.Method (resume G R))
          ].
    End Impl_core_ops_coroutine_Coroutine_where_core_marker_Sized_G_where_core_ops_coroutine_Coroutine_G_R_where_core_marker_Unpin_G_R_for_ref_mut_G.
  End coroutine.
End ops.
