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

Module ops.
  Module control_flow.
    (*
    Enum ControlFlow
    {
      const_params := [];
      ty_params := [ "B"; "C" ];
      variants :=
        [
          {
            name := "Continue";
            item := StructTuple [ C ];
            discriminant := None;
          };
          {
            name := "Break";
            item := StructTuple [ B ];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_B_where_core_fmt_Debug_C_for_core_ops_control_flow_ControlFlow_B_C.
      Definition Self (B C : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ B; C ].
      
      (* Debug *)
      Definition fmt (B C : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self B C 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::control_flow::ControlFlow::Continue",
                          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 "Continue" |); __self_0 ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Break",
                          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 "Break" |); __self_0 ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (B C : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self B C)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt B C)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_B_where_core_fmt_Debug_C_for_core_ops_control_flow_ControlFlow_B_C.
    
    Module Impl_core_clone_Clone_where_core_clone_Clone_B_where_core_clone_Clone_C_for_core_ops_control_flow_ControlFlow_B_C.
      Definition Self (B C : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ B; C ].
      
      (* Clone *)
      Definition clone (B C : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self B C 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::control_flow::ControlFlow::Continue",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::control_flow::ControlFlow::Continue"
                          [
                            M.call_closure (|
                              M.get_trait_method (| "core::clone::Clone", C, [], "clone", [] |),
                              [ M.read (| __self_0 |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Break",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::control_flow::ControlFlow::Break"
                          [
                            M.call_closure (|
                              M.get_trait_method (| "core::clone::Clone", B, [], "clone", [] |),
                              [ M.read (| __self_0 |) ]
                            |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (B C : Ty.t),
        M.IsTraitInstance
          "core::clone::Clone"
          (Self B C)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method (clone B C)) ].
    End Impl_core_clone_Clone_where_core_clone_Clone_B_where_core_clone_Clone_C_for_core_ops_control_flow_ControlFlow_B_C.
    
    Module Impl_core_marker_Copy_where_core_marker_Copy_B_where_core_marker_Copy_C_for_core_ops_control_flow_ControlFlow_B_C.
      Definition Self (B C : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ B; C ].
      
      Axiom Implements :
        forall (B C : Ty.t),
        M.IsTraitInstance
          "core::marker::Copy"
          (Self B C)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_where_core_marker_Copy_B_where_core_marker_Copy_C_for_core_ops_control_flow_ControlFlow_B_C.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_ops_control_flow_ControlFlow_B_C.
      Definition Self (B C : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ B; C ].
      
      Axiom Implements :
        forall (B C : Ty.t),
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          (Self B C)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_ops_control_flow_ControlFlow_B_C.
    
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_B_where_core_cmp_PartialEq_C_for_core_ops_control_flow_ControlFlow_B_C.
      Definition Self (B C : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ B; C ].
      
      (* PartialEq *)
      Definition eq (B C : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self B C 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::control_flow::ControlFlow") [] [ B; C ] ]
                    |),
                    [ 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::control_flow::ControlFlow") [] [ B; C ] ]
                    |),
                    [ 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::control_flow::ControlFlow::Continue",
                                  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::control_flow::ControlFlow::Continue",
                                  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 "&") [] [ C ],
                                    [ Ty.apply (Ty.path "&") [] [ C ] ],
                                    "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::control_flow::ControlFlow::Break",
                                  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::control_flow::ControlFlow::Break",
                                  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 "&") [] [ B ],
                                    [ Ty.apply (Ty.path "&") [] [ B ] ],
                                    "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 (B C : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self B C)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method (eq B C)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_B_where_core_cmp_PartialEq_C_for_core_ops_control_flow_ControlFlow_B_C.
    
    Module Impl_core_cmp_Eq_where_core_cmp_Eq_B_where_core_cmp_Eq_C_for_core_ops_control_flow_ControlFlow_B_C.
      Definition Self (B C : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ B; C ].
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (B C : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self B C 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 (B C : Ty.t),
        M.IsTraitInstance
          "core::cmp::Eq"
          (Self B C)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method (assert_receiver_is_total_eq B C))
          ].
    End Impl_core_cmp_Eq_where_core_cmp_Eq_B_where_core_cmp_Eq_C_for_core_ops_control_flow_ControlFlow_B_C.
    
    Module Impl_core_hash_Hash_where_core_hash_Hash_B_where_core_hash_Hash_C_for_core_ops_control_flow_ControlFlow_B_C.
      Definition Self (B C : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ B; C ].
      
      (* Hash *)
      Definition hash (B C : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self B C 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::control_flow::ControlFlow") [] [ B; C ] ]
                    |),
                    [ 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::control_flow::ControlFlow::Continue",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (| "core::hash::Hash", C, [], "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::control_flow::ControlFlow::Break",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (| "core::hash::Hash", B, [], "hash", [ __H ] |),
                          [ M.read (| __self_0 |); M.read (| state |) ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (B C : Ty.t),
        M.IsTraitInstance
          "core::hash::Hash"
          (Self B C)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("hash", InstanceField.Method (hash B C)) ].
    End Impl_core_hash_Hash_where_core_hash_Hash_B_where_core_hash_Hash_C_for_core_ops_control_flow_ControlFlow_B_C.
    
    Module Impl_core_ops_try_trait_Try_for_core_ops_control_flow_ControlFlow_B_C.
      Definition Self (B C : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ B; C ].
      
      (*     type Output = C; *)
      Definition _Output (B C : Ty.t) : Ty.t := C.
      
      (*     type Residual = ControlFlow<B, convert::Infallible>; *)
      Definition _Residual (B C : Ty.t) : Ty.t :=
        Ty.apply
          (Ty.path "core::ops::control_flow::ControlFlow")
          []
          [ B; Ty.path "core::convert::Infallible" ].
      
      (*
          fn from_output(output: Self::Output) -> Self {
              ControlFlow::Continue(output)
          }
      *)
      Definition from_output
          (B C : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self B C in
        match ε, τ, α with
        | [], [], [ output ] =>
          ltac:(M.monadic
            (let output := M.alloc (| output |) in
            Value.StructTuple
              "core::ops::control_flow::ControlFlow::Continue"
              [ M.read (| output |) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn branch(self) -> ControlFlow<Self::Residual, Self::Output> {
              match self {
                  ControlFlow::Continue(c) => ControlFlow::Continue(c),
                  ControlFlow::Break(b) => ControlFlow::Break(ControlFlow::Break(b)),
              }
          }
      *)
      Definition branch (B C : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self B C in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Continue",
                          0
                        |) in
                      let c := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::control_flow::ControlFlow::Continue"
                          [ M.read (| c |) ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Break",
                          0
                        |) in
                      let b := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::control_flow::ControlFlow::Break"
                          [
                            Value.StructTuple
                              "core::ops::control_flow::ControlFlow::Break"
                              [ M.read (| b |) ]
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (B C : Ty.t),
        M.IsTraitInstance
          "core::ops::try_trait::Try"
          (Self B C)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Output", InstanceField.Ty (_Output B C));
            ("Residual", InstanceField.Ty (_Residual B C));
            ("from_output", InstanceField.Method (from_output B C));
            ("branch", InstanceField.Method (branch B C))
          ].
    End Impl_core_ops_try_trait_Try_for_core_ops_control_flow_ControlFlow_B_C.
    
    Module Impl_core_ops_try_trait_FromResidual_core_ops_control_flow_ControlFlow_B_core_convert_Infallible_for_core_ops_control_flow_ControlFlow_B_C.
      Definition Self (B C : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ B; C ].
      
      (*
          fn from_residual(residual: ControlFlow<B, convert::Infallible>) -> Self {
              match residual {
                  ControlFlow::Break(b) => ControlFlow::Break(b),
              }
          }
      *)
      Definition from_residual
          (B C : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self B C in
        match ε, τ, α with
        | [], [], [ residual ] =>
          ltac:(M.monadic
            (let residual := M.alloc (| residual |) in
            M.read (|
              M.match_operator (|
                residual,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Break",
                          0
                        |) in
                      let b := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::control_flow::ControlFlow::Break"
                          [ M.read (| b |) ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (B C : Ty.t),
        M.IsTraitInstance
          "core::ops::try_trait::FromResidual"
          (Self B C)
          (* Trait polymorphic types *)
          [
            (* R *)
            Ty.apply
              (Ty.path "core::ops::control_flow::ControlFlow")
              []
              [ B; Ty.path "core::convert::Infallible" ]
          ]
          (* Instance *) [ ("from_residual", InstanceField.Method (from_residual B C)) ].
    End Impl_core_ops_try_trait_FromResidual_core_ops_control_flow_ControlFlow_B_core_convert_Infallible_for_core_ops_control_flow_ControlFlow_B_C.
    
    Module Impl_core_ops_try_trait_Residual_C_for_core_ops_control_flow_ControlFlow_B_core_convert_Infallible.
      Definition Self (B C : Ty.t) : Ty.t :=
        Ty.apply
          (Ty.path "core::ops::control_flow::ControlFlow")
          []
          [ B; Ty.path "core::convert::Infallible" ].
      
      (*     type TryType = ControlFlow<B, C>; *)
      Definition _TryType (B C : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ B; C ].
      
      Axiom Implements :
        forall (B C : Ty.t),
        M.IsTraitInstance
          "core::ops::try_trait::Residual"
          (Self B C)
          (* Trait polymorphic types *) [ (* O *) C ]
          (* Instance *) [ ("TryType", InstanceField.Ty (_TryType B C)) ].
    End Impl_core_ops_try_trait_Residual_C_for_core_ops_control_flow_ControlFlow_B_core_convert_Infallible.
    
    Module Impl_core_ops_control_flow_ControlFlow_B_C.
      Definition Self (B C : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ B; C ].
      
      (*
          pub fn is_break(&self) -> bool {
              matches!( *self, ControlFlow::Break(_))
          }
      *)
      Definition is_break (B C : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self B C in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.read (| self |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Break",
                          0
                        |) in
                      M.alloc (| Value.Bool true |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_break :
        forall (B C : Ty.t),
        M.IsAssociatedFunction (Self B C) "is_break" (is_break B C).
      
      (*
          pub fn is_continue(&self) -> bool {
              matches!( *self, ControlFlow::Continue(_))
          }
      *)
      Definition is_continue
          (B C : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self B C in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.read (| self |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Continue",
                          0
                        |) in
                      M.alloc (| Value.Bool true |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_continue :
        forall (B C : Ty.t),
        M.IsAssociatedFunction (Self B C) "is_continue" (is_continue B C).
      
      (*
          pub fn break_value(self) -> Option<B> {
              match self {
                  ControlFlow::Continue(..) => None,
                  ControlFlow::Break(x) => Some(x),
              }
          }
      *)
      Definition break_value
          (B C : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self B C 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.is_struct_tuple (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Continue"
                        |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Break",
                          0
                        |) in
                      let x := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple "core::option::Option::Some" [ M.read (| x |) ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_break_value :
        forall (B C : Ty.t),
        M.IsAssociatedFunction (Self B C) "break_value" (break_value B C).
      
      (*
          pub fn map_break<T, F>(self, f: F) -> ControlFlow<T, C>
          where
              F: FnOnce(B) -> T,
          {
              match self {
                  ControlFlow::Continue(x) => ControlFlow::Continue(x),
                  ControlFlow::Break(x) => ControlFlow::Break(f(x)),
              }
          }
      *)
      Definition map_break (B C : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self B C in
        match ε, τ, α with
        | [], [ T; F ], [ 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 γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Continue",
                          0
                        |) in
                      let x := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::control_flow::ControlFlow::Continue"
                          [ M.read (| x |) ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Break",
                          0
                        |) in
                      let x := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::control_flow::ControlFlow::Break"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::function::FnOnce",
                                F,
                                [ Ty.tuple [ B ] ],
                                "call_once",
                                []
                              |),
                              [ M.read (| f |); Value.Tuple [ M.read (| x |) ] ]
                            |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_map_break :
        forall (B C : Ty.t),
        M.IsAssociatedFunction (Self B C) "map_break" (map_break B C).
      
      (*
          pub fn continue_value(self) -> Option<C> {
              match self {
                  ControlFlow::Continue(x) => Some(x),
                  ControlFlow::Break(..) => None,
              }
          }
      *)
      Definition continue_value
          (B C : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self B C in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Continue",
                          0
                        |) in
                      let x := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple "core::option::Option::Some" [ M.read (| x |) ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (| γ, "core::ops::control_flow::ControlFlow::Break" |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_continue_value :
        forall (B C : Ty.t),
        M.IsAssociatedFunction (Self B C) "continue_value" (continue_value B C).
      
      (*
          pub fn map_continue<T, F>(self, f: F) -> ControlFlow<B, T>
          where
              F: FnOnce(C) -> T,
          {
              match self {
                  ControlFlow::Continue(x) => ControlFlow::Continue(f(x)),
                  ControlFlow::Break(x) => ControlFlow::Break(x),
              }
          }
      *)
      Definition map_continue
          (B C : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self B C in
        match ε, τ, α with
        | [], [ T; F ], [ 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 γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Continue",
                          0
                        |) in
                      let x := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::control_flow::ControlFlow::Continue"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::function::FnOnce",
                                F,
                                [ Ty.tuple [ C ] ],
                                "call_once",
                                []
                              |),
                              [ M.read (| f |); Value.Tuple [ M.read (| x |) ] ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Break",
                          0
                        |) in
                      let x := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::control_flow::ControlFlow::Break"
                          [ M.read (| x |) ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_map_continue :
        forall (B C : Ty.t),
        M.IsAssociatedFunction (Self B C) "map_continue" (map_continue B C).
    End Impl_core_ops_control_flow_ControlFlow_B_C.
    
    Module Impl_core_ops_control_flow_ControlFlow_R_associated_type.
      Definition Self (R : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::ops::control_flow::ControlFlow") [] [ R; Ty.associated ].
      
      (*
          pub(crate) fn from_try(r: R) -> Self {
              match R::branch(r) {
                  ControlFlow::Continue(v) => ControlFlow::Continue(v),
                  ControlFlow::Break(v) => ControlFlow::Break(R::from_residual(v)),
              }
          }
      *)
      Definition from_try (R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self R in
        match ε, τ, α with
        | [], [], [ r ] =>
          ltac:(M.monadic
            (let r := M.alloc (| r |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (| "core::ops::try_trait::Try", R, [], "branch", [] |),
                    [ M.read (| r |) ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Continue",
                          0
                        |) in
                      let v := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::control_flow::ControlFlow::Continue"
                          [ M.read (| v |) ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Break",
                          0
                        |) in
                      let v := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::ops::control_flow::ControlFlow::Break"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::FromResidual",
                                R,
                                [ Ty.associated ],
                                "from_residual",
                                []
                              |),
                              [ M.read (| v |) ]
                            |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_try :
        forall (R : Ty.t),
        M.IsAssociatedFunction (Self R) "from_try" (from_try R).
      
      (*
          pub(crate) fn into_try(self) -> R {
              match self {
                  ControlFlow::Continue(v) => R::from_output(v),
                  ControlFlow::Break(v) => v,
              }
          }
      *)
      Definition into_try (R : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self 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 γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Continue",
                          0
                        |) in
                      let v := M.copy (| γ0_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            R,
                            [],
                            "from_output",
                            []
                          |),
                          [ M.read (| v |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::ops::control_flow::ControlFlow::Break",
                          0
                        |) in
                      let v := M.copy (| γ0_0 |) in
                      v))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_into_try :
        forall (R : Ty.t),
        M.IsAssociatedFunction (Self R) "into_try" (into_try R).
    End Impl_core_ops_control_flow_ControlFlow_R_associated_type.
  End control_flow.
End ops.
