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

Module result.
  (*
  Enum Result
  {
    const_params := [];
    ty_params := [ "T"; "E" ];
    variants :=
      [
        {
          name := "Ok";
          item := StructTuple [ T ];
          discriminant := None;
        };
        {
          name := "Err";
          item := StructTuple [ E ];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_marker_Copy_where_core_marker_Copy_T_where_core_marker_Copy_E_for_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    Axiom Implements :
      forall (T E : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_where_core_marker_Copy_T_where_core_marker_Copy_E_for_core_result_Result_T_E.
  
  Module Impl_core_marker_StructuralPartialEq_for_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    Axiom Implements :
      forall (T E : Ty.t),
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_result_Result_T_E.
  
  Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_where_core_cmp_PartialEq_E_for_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    (* PartialEq *)
    Definition eq (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result") [] [ T; E ] ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.apply (Ty.path "core::result::Result") [] [ T; E ] ]
                  |),
                  [ 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::result::Result::Ok",
                                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::result::Result::Ok",
                                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 "&") [] [ T ],
                                  [ Ty.apply (Ty.path "&") [] [ T ] ],
                                  "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::result::Result::Err",
                                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::result::Result::Err",
                                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 "&") [] [ E ],
                                  [ Ty.apply (Ty.path "&") [] [ E ] ],
                                  "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 (T E : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialEq"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method (eq T E)) ].
  End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_where_core_cmp_PartialEq_E_for_core_result_Result_T_E.
  
  Module Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_T_where_core_cmp_PartialOrd_E_for_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    (* PartialOrd *)
    Definition partial_cmp (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result") [] [ T; E ] ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.apply (Ty.path "core::result::Result") [] [ T; E ] ]
                  |),
                  [ 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::result::Result::Ok",
                        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::result::Result::Ok",
                        0
                      |) in
                    let __arg1_0 := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialOrd",
                          T,
                          [ T ],
                          "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::result::Result::Err",
                        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::result::Result::Err",
                        0
                      |) in
                    let __arg1_0 := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialOrd",
                          E,
                          [ E ],
                          "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 (T E : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method (partial_cmp T E)) ].
  End Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_T_where_core_cmp_PartialOrd_E_for_core_result_Result_T_E.
  
  Module Impl_core_cmp_Eq_where_core_cmp_Eq_T_where_core_cmp_Eq_E_for_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (T E : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T E 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 (T E : Ty.t),
      M.IsTraitInstance
        "core::cmp::Eq"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method (assert_receiver_is_total_eq T E)) ].
  End Impl_core_cmp_Eq_where_core_cmp_Eq_T_where_core_cmp_Eq_E_for_core_result_Result_T_E.
  
  Module Impl_core_cmp_Ord_where_core_cmp_Ord_T_where_core_cmp_Ord_E_for_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    (* Ord *)
    Definition cmp (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result") [] [ T; E ] ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.apply (Ty.path "core::result::Result") [] [ T; E ] ]
                  |),
                  [ 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::result::Result::Ok",
                                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::result::Result::Ok",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (| "core::cmp::Ord", T, [], "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::result::Result::Err",
                                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::result::Result::Err",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (| "core::cmp::Ord", E, [], "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 (T E : Ty.t),
      M.IsTraitInstance
        "core::cmp::Ord"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method (cmp T E)) ].
  End Impl_core_cmp_Ord_where_core_cmp_Ord_T_where_core_cmp_Ord_E_for_core_result_Result_T_E.
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_fmt_Debug_E_for_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    (* Debug *)
    Definition fmt (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 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 "Ok" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 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 "Err" |); __self_0 ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T E : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt T E)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_fmt_Debug_E_for_core_result_Result_T_E.
  
  Module Impl_core_hash_Hash_where_core_hash_Hash_T_where_core_hash_Hash_E_for_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    (* Hash *)
    Definition hash (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result") [] [ T; E ] ]
                  |),
                  [ 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::result::Result::Ok", 0 |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::hash::Hash", T, [], "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::result::Result::Err", 0 |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::hash::Hash", E, [], "hash", [ __H ] |),
                        [ M.read (| __self_0 |); M.read (| state |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T E : Ty.t),
      M.IsTraitInstance
        "core::hash::Hash"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method (hash T E)) ].
  End Impl_core_hash_Hash_where_core_hash_Hash_T_where_core_hash_Hash_E_for_core_result_Result_T_E.
  
  Module Impl_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    (*
        pub const fn is_ok(&self) -> bool {
            matches!( *self, Ok(_))
        }
    *)
    Definition is_ok (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 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_ok :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "is_ok" (is_ok T E).
    
    (*
        pub fn is_ok_and(self, f: impl FnOnce(T) -> bool) -> bool {
            match self {
                Err(_) => false,
                Ok(x) => f(x),
            }
        }
    *)
    Definition is_ok_and (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ impl_FnOnce_T__arrow_bool ], [ 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::result::Result::Err", 0 |) in
                    M.alloc (| Value.Bool false |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let x := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          impl_FnOnce_T__arrow_bool,
                          [ Ty.tuple [ T ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| f |); Value.Tuple [ M.read (| x |) ] ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_ok_and :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "is_ok_and" (is_ok_and T E).
    
    (*
        pub const fn is_err(&self) -> bool {
            !self.is_ok()
        }
    *)
    Definition is_err (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          UnOp.not (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::result::Result") [] [ T; E ],
                "is_ok",
                []
              |),
              [ M.read (| self |) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_err :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "is_err" (is_err T E).
    
    (*
        pub fn is_err_and(self, f: impl FnOnce(E) -> bool) -> bool {
            match self {
                Ok(_) => false,
                Err(e) => f(e),
            }
        }
    *)
    Definition is_err_and (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ impl_FnOnce_E__arrow_bool ], [ 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::result::Result::Ok", 0 |) in
                    M.alloc (| Value.Bool false |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          impl_FnOnce_E__arrow_bool,
                          [ Ty.tuple [ E ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| f |); Value.Tuple [ M.read (| e |) ] ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_err_and :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "is_err_and" (is_err_and T E).
    
    (*
        pub fn ok(self) -> Option<T> {
            match self {
                Ok(x) => Some(x),
                Err(_) => None,
            }
        }
    *)
    Definition ok (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 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 γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_ok :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "ok" (ok T E).
    
    (*
        pub fn err(self) -> Option<E> {
            match self {
                Ok(_) => None,
                Err(x) => Some(x),
            }
        }
    *)
    Definition err (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 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_err :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "err" (err T E).
    
    (*
        pub const fn as_ref(&self) -> Result<&T, &E> {
            match *self {
                Ok(ref x) => Ok(x),
                Err(ref x) => Err(x),
            }
        }
    *)
    Definition as_ref (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let x := M.alloc (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| x |) ] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let x := M.alloc (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Err" [ M.read (| x |) ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_ref :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "as_ref" (as_ref T E).
    
    (*
        pub const fn as_mut(&mut self) -> Result<&mut T, &mut E> {
            match *self {
                Ok(ref mut x) => Ok(x),
                Err(ref mut x) => Err(x),
            }
        }
    *)
    Definition as_mut (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let x := M.alloc (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| x |) ] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let x := M.alloc (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Err" [ M.read (| x |) ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_mut :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "as_mut" (as_mut T E).
    
    (*
        pub fn map<U, F: FnOnce(T) -> U>(self, op: F) -> Result<U, E> {
            match self {
                Ok(t) => Ok(op(t)),
                Err(e) => Err(e),
            }
        }
    *)
    Definition map (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ U; F ], [ self; op ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let op := M.alloc (| op |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::function::FnOnce",
                              F,
                              [ Ty.tuple [ T ] ],
                              "call_once",
                              []
                            |),
                            [ M.read (| op |); Value.Tuple [ M.read (| t |) ] ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Err" [ M.read (| e |) ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "map" (map T E).
    
    (*
        pub fn map_or<U, F: FnOnce(T) -> U>(self, default: U, f: F) -> U {
            match self {
                Ok(t) => f(t),
                Err(_) => default,
            }
        }
    *)
    Definition map_or (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ U; F ], [ self; default; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let default := M.alloc (| default |) 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::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          F,
                          [ Ty.tuple [ T ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| f |); Value.Tuple [ M.read (| t |) ] ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    default))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map_or :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "map_or" (map_or T E).
    
    (*
        pub fn map_or_else<U, D: FnOnce(E) -> U, F: FnOnce(T) -> U>(self, default: D, f: F) -> U {
            match self {
                Ok(t) => f(t),
                Err(e) => default(e),
            }
        }
    *)
    Definition map_or_else (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ U; D; F ], [ self; default; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let default := M.alloc (| default |) 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::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          F,
                          [ Ty.tuple [ T ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| f |); Value.Tuple [ M.read (| t |) ] ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          D,
                          [ Ty.tuple [ E ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| default |); Value.Tuple [ M.read (| e |) ] ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map_or_else :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "map_or_else" (map_or_else T E).
    
    (*
        pub fn map_err<F, O: FnOnce(E) -> F>(self, op: O) -> Result<T, F> {
            match self {
                Ok(t) => Ok(t),
                Err(e) => Err(op(e)),
            }
        }
    *)
    Definition map_err (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ F; _ as O ], [ self; op ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let op := M.alloc (| op |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| t |) ] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::function::FnOnce",
                              O,
                              [ Ty.tuple [ E ] ],
                              "call_once",
                              []
                            |),
                            [ M.read (| op |); Value.Tuple [ M.read (| e |) ] ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map_err :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "map_err" (map_err T E).
    
    (*
        pub fn inspect<F: FnOnce(&T)>(self, f: F) -> Self {
            if let Ok(ref t) = self {
                f(t);
            }
    
            self
        }
    *)
    Definition inspect (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ F ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := self in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Ok",
                          0
                        |) in
                      let t := M.alloc (| γ0_0 |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::function::FnOnce",
                              F,
                              [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                              "call_once",
                              []
                            |),
                            [ M.read (| f |); Value.Tuple [ M.read (| t |) ] ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_inspect :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "inspect" (inspect T E).
    
    (*
        pub fn inspect_err<F: FnOnce(&E)>(self, f: F) -> Self {
            if let Err(ref e) = self {
                f(e);
            }
    
            self
        }
    *)
    Definition inspect_err (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ F ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := self in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Err",
                          0
                        |) in
                      let e := M.alloc (| γ0_0 |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::function::FnOnce",
                              F,
                              [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ E ] ] ],
                              "call_once",
                              []
                            |),
                            [ M.read (| f |); Value.Tuple [ M.read (| e |) ] ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_inspect_err :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "inspect_err" (inspect_err T E).
    
    (*
        pub fn as_deref(&self) -> Result<&T::Target, &E>
        where
            T: Deref,
        {
            self.as_ref().map(|t| t.deref())
        }
    *)
    Definition as_deref (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ E ] ],
              "map",
              [
                Ty.apply (Ty.path "&") [] [ Ty.associated ];
                Ty.function
                  [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ]
                  (Ty.apply (Ty.path "&") [] [ Ty.associated ])
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::result::Result") [] [ T; E ],
                  "as_ref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let t := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::Deref",
                                    T,
                                    [],
                                    "deref",
                                    []
                                  |),
                                  [ M.read (| t |) ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_deref :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "as_deref" (as_deref T E).
    
    (*
        pub fn as_deref_mut(&mut self) -> Result<&mut T::Target, &mut E>
        where
            T: DerefMut,
        {
            self.as_mut().map(|t| t.deref_mut())
        }
    *)
    Definition as_deref_mut
        (T E : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [ Ty.apply (Ty.path "&mut") [] [ T ]; Ty.apply (Ty.path "&mut") [] [ E ] ],
              "map",
              [
                Ty.apply (Ty.path "&mut") [] [ Ty.associated ];
                Ty.function
                  [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ T ] ] ]
                  (Ty.apply (Ty.path "&mut") [] [ Ty.associated ])
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::result::Result") [] [ T; E ],
                  "as_mut",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let t := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::DerefMut",
                                    T,
                                    [],
                                    "deref_mut",
                                    []
                                  |),
                                  [ M.read (| t |) ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_deref_mut :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "as_deref_mut" (as_deref_mut T E).
    
    (*
        pub fn iter(&self) -> Iter<'_, T> {
            Iter { inner: self.as_ref().ok() }
        }
    *)
    Definition iter (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::result::Iter"
            [
              ("inner",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::result::Result")
                      []
                      [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ E ] ],
                    "ok",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::result::Result") [] [ T; E ],
                        "as_ref",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_iter :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "iter" (iter T E).
    
    (*
        pub fn iter_mut(&mut self) -> IterMut<'_, T> {
            IterMut { inner: self.as_mut().ok() }
        }
    *)
    Definition iter_mut (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::result::IterMut"
            [
              ("inner",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::result::Result")
                      []
                      [ Ty.apply (Ty.path "&mut") [] [ T ]; Ty.apply (Ty.path "&mut") [] [ E ] ],
                    "ok",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::result::Result") [] [ T; E ],
                        "as_mut",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_iter_mut :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "iter_mut" (iter_mut T E).
    
    (*
        pub fn expect(self, msg: &str) -> T
        where
            E: fmt::Debug,
        {
            match self {
                Ok(t) => t,
                Err(e) => unwrap_failed(msg, &e),
            }
        }
    *)
    Definition expect (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self; msg ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let msg := M.alloc (| msg |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    t));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::result::unwrap_failed", [] |),
                          [ M.read (| msg |); e ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_expect :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "expect" (expect T E).
    
    (*
        pub fn unwrap(self) -> T
        where
            E: fmt::Debug,
        {
            match self {
                Ok(t) => t,
                Err(e) => unwrap_failed("called `Result::unwrap()` on an `Err` value", &e),
            }
        }
    *)
    Definition unwrap (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    t));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::result::unwrap_failed", [] |),
                          [
                            M.read (| Value.String "called `Result::unwrap()` on an `Err` value" |);
                            e
                          ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unwrap :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "unwrap" (unwrap T E).
    
    (*
        pub fn unwrap_or_default(self) -> T
        where
            T: Default,
        {
            match self {
                Ok(x) => x,
                Err(_) => Default::default(),
            }
        }
    *)
    Definition unwrap_or_default
        (T E : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let x := M.copy (| γ0_0 |) in
                    x));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                        []
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unwrap_or_default :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "unwrap_or_default" (unwrap_or_default T E).
    
    (*
        pub fn expect_err(self, msg: &str) -> E
        where
            T: fmt::Debug,
        {
            match self {
                Ok(t) => unwrap_failed(msg, &t),
                Err(e) => e,
            }
        }
    *)
    Definition expect_err (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self; msg ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let msg := M.alloc (| msg |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::result::unwrap_failed", [] |),
                          [ M.read (| msg |); t ]
                        |)
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    e))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_expect_err :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "expect_err" (expect_err T E).
    
    (*
        pub fn unwrap_err(self) -> E
        where
            T: fmt::Debug,
        {
            match self {
                Ok(t) => unwrap_failed("called `Result::unwrap_err()` on an `Ok` value", &t),
                Err(e) => e,
            }
        }
    *)
    Definition unwrap_err (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::result::unwrap_failed", [] |),
                          [
                            M.read (|
                              Value.String "called `Result::unwrap_err()` on an `Ok` value"
                            |);
                            t
                          ]
                        |)
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    e))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unwrap_err :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "unwrap_err" (unwrap_err T E).
    
    (*
        pub fn into_ok(self) -> T
        where
            E: Into<!>,
        {
            match self {
                Ok(x) => x,
                Err(e) => e.into(),
            }
        }
    *)
    Definition into_ok (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let x := M.copy (| γ0_0 |) in
                    x));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::convert::Into",
                            E,
                            [ Ty.path "never" ],
                            "into",
                            []
                          |),
                          [ M.read (| e |) ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_ok :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "into_ok" (into_ok T E).
    
    (*
        pub fn into_err(self) -> E
        where
            T: Into<!>,
        {
            match self {
                Ok(x) => x.into(),
                Err(e) => e,
            }
        }
    *)
    Definition into_err (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let x := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::convert::Into",
                            T,
                            [ Ty.path "never" ],
                            "into",
                            []
                          |),
                          [ M.read (| x |) ]
                        |)
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    e))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_err :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "into_err" (into_err T E).
    
    (*
        pub fn and<U>(self, res: Result<U, E>) -> Result<U, E> {
            match self {
                Ok(_) => res,
                Err(e) => Err(e),
            }
        }
    *)
    Definition and (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ U ], [ self; res ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let res := M.alloc (| res |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    res));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Err" [ M.read (| e |) ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_and :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "and" (and T E).
    
    (*
        pub fn and_then<U, F: FnOnce(T) -> Result<U, E>>(self, op: F) -> Result<U, E> {
            match self {
                Ok(t) => op(t),
                Err(e) => Err(e),
            }
        }
    *)
    Definition and_then (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ U; F ], [ self; op ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let op := M.alloc (| op |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          F,
                          [ Ty.tuple [ T ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| op |); Value.Tuple [ M.read (| t |) ] ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Err" [ M.read (| e |) ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_and_then :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "and_then" (and_then T E).
    
    (*
        pub fn or<F>(self, res: Result<T, F>) -> Result<T, F> {
            match self {
                Ok(v) => Ok(v),
                Err(_) => res,
            }
        }
    *)
    Definition or (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ F ], [ self; res ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let res := M.alloc (| res |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let v := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| v |) ] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    res))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_or :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "or" (or T E).
    
    (*
        pub fn or_else<F, O: FnOnce(E) -> Result<T, F>>(self, op: O) -> Result<T, F> {
            match self {
                Ok(t) => Ok(t),
                Err(e) => op(e),
            }
        }
    *)
    Definition or_else (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ F; _ as O ], [ self; op ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let op := M.alloc (| op |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| t |) ] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          O,
                          [ Ty.tuple [ E ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| op |); Value.Tuple [ M.read (| e |) ] ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_or_else :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "or_else" (or_else T E).
    
    (*
        pub fn unwrap_or(self, default: T) -> T {
            match self {
                Ok(t) => t,
                Err(_) => default,
            }
        }
    *)
    Definition unwrap_or (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self; default ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let default := M.alloc (| default |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    t));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    default))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unwrap_or :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "unwrap_or" (unwrap_or T E).
    
    (*
        pub fn unwrap_or_else<F: FnOnce(E) -> T>(self, op: F) -> T {
            match self {
                Ok(t) => t,
                Err(e) => op(e),
            }
        }
    *)
    Definition unwrap_or_else
        (T E : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [ F ], [ self; op ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let op := M.alloc (| op |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    t));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          F,
                          [ Ty.tuple [ E ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| op |); Value.Tuple [ M.read (| e |) ] ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unwrap_or_else :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "unwrap_or_else" (unwrap_or_else T E).
    
    (*
        pub unsafe fn unwrap_unchecked(self) -> T {
            match self {
                Ok(t) => t,
                // SAFETY: the safety contract must be upheld by the caller.
                Err(_) => unsafe { hint::unreachable_unchecked() },
            }
        }
    *)
    Definition unwrap_unchecked
        (T E : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let t := M.copy (| γ0_0 |) in
                    t));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::hint::unreachable_unchecked", [] |),
                          []
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unwrap_unchecked :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "unwrap_unchecked" (unwrap_unchecked T E).
    
    (*
        pub unsafe fn unwrap_err_unchecked(self) -> E {
            match self {
                // SAFETY: the safety contract must be upheld by the caller.
                Ok(_) => unsafe { hint::unreachable_unchecked() },
                Err(e) => e,
            }
        }
    *)
    Definition unwrap_err_unchecked
        (T E : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::hint::unreachable_unchecked", [] |),
                          []
                        |)
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    e))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unwrap_err_unchecked :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "unwrap_err_unchecked" (unwrap_err_unchecked T E).
  End Impl_core_result_Result_T_E.
  
  Module Impl_core_result_Result_ref__T_E.
    Definition Self (T E : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::result::Result") [] [ Ty.apply (Ty.path "&") [] [ T ]; E ].
    
    (*
        pub const fn copied(self) -> Result<T, E>
        where
            T: Copy,
        {
            // FIXME(const-hack): this implementation, which sidesteps using `Result::map` since it's not const
            // ready yet, should be reverted when possible to avoid code repetition
            match self {
                Ok(&v) => Ok(v),
                Err(e) => Err(e),
            }
        }
    *)
    Definition copied (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let γ0_0 := M.read (| γ0_0 |) in
                    let v := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| v |) ] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Err" [ M.read (| e |) ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_copied :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "copied" (copied T E).
    
    (*
        pub fn cloned(self) -> Result<T, E>
        where
            T: Clone,
        {
            self.map(|t| t.clone())
        }
    *)
    Definition cloned (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::result::Result") [] [ Ty.apply (Ty.path "&") [] [ T ]; E ],
              "map",
              [ T; Ty.function [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ] T ]
            |),
            [
              M.read (| self |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let t := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                                  [ M.read (| t |) ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_cloned :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "cloned" (cloned T E).
  End Impl_core_result_Result_ref__T_E.
  
  Module Impl_core_result_Result_ref_mut_T_E.
    Definition Self (T E : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::result::Result") [] [ Ty.apply (Ty.path "&mut") [] [ T ]; E ].
    
    (*
        pub const fn copied(self) -> Result<T, E>
        where
            T: Copy,
        {
            // FIXME(const-hack): this implementation, which sidesteps using `Result::map` since it's not const
            // ready yet, should be reverted when possible to avoid code repetition
            match self {
                Ok(&mut v) => Ok(v),
                Err(e) => Err(e),
            }
        }
    *)
    Definition copied (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let γ0_0 := M.read (| γ0_0 |) in
                    let v := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| v |) ] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Err" [ M.read (| e |) ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_copied :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "copied" (copied T E).
    
    (*
        pub fn cloned(self) -> Result<T, E>
        where
            T: Clone,
        {
            self.map(|t| t.clone())
        }
    *)
    Definition cloned (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [ Ty.apply (Ty.path "&mut") [] [ T ]; E ],
              "map",
              [ T; Ty.function [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ T ] ] ] T ]
            |),
            [
              M.read (| self |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let t := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                                  [ M.read (| t |) ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_cloned :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "cloned" (cloned T E).
  End Impl_core_result_Result_ref_mut_T_E.
  
  Module Impl_core_result_Result_core_option_Option_T_E.
    Definition Self (T E : Ty.t) : Ty.t :=
      Ty.apply
        (Ty.path "core::result::Result")
        []
        [ Ty.apply (Ty.path "core::option::Option") [] [ T ]; E ].
    
    (*
        pub const fn transpose(self) -> Option<Result<T, E>> {
            match self {
                Ok(Some(x)) => Some(Ok(x)),
                Ok(None) => None,
                Err(e) => Some(Err(e)),
            }
        }
    *)
    Definition transpose (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [ Value.StructTuple "core::result::Result::Ok" [ M.read (| x |) ] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [ Value.StructTuple "core::result::Result::Err" [ M.read (| e |) ] ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_transpose :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "transpose" (transpose T E).
  End Impl_core_result_Result_core_option_Option_T_E.
  
  Module Impl_core_result_Result_core_result_Result_T_E_E.
    Definition Self (T E : Ty.t) : Ty.t :=
      Ty.apply
        (Ty.path "core::result::Result")
        []
        [ Ty.apply (Ty.path "core::result::Result") [] [ T; E ]; E ].
    
    (*
        pub const fn flatten(self) -> Result<T, E> {
            // FIXME(const-hack): could be written with `and_then`
            match self {
                Ok(inner) => inner,
                Err(e) => Err(e),
            }
        }
    *)
    Definition flatten (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let inner := M.copy (| γ0_0 |) in
                    inner));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Err" [ M.read (| e |) ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_flatten :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "flatten" (flatten T E).
  End Impl_core_result_Result_core_result_Result_T_E_E.
  
  (*
  fn unwrap_failed(msg: &str, error: &dyn fmt::Debug) -> ! {
      panic!("{msg}: {error:?}")
  }
  *)
  Definition unwrap_failed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ msg; error ] =>
      ltac:(M.monadic
        (let msg := M.alloc (| msg |) in
        let error := M.alloc (| error |) in
        M.call_closure (|
          M.get_function (| "core::panicking::panic_fmt", [] |),
          [
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
              [
                M.alloc (|
                  Value.Array [ M.read (| Value.String "" |); M.read (| Value.String ": " |) ]
                |);
                M.alloc (|
                  Value.Array
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::rt::Argument",
                          "new_display",
                          [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                        |),
                        [ msg ]
                      |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::rt::Argument",
                          "new_debug",
                          [ Ty.apply (Ty.path "&") [] [ Ty.dyn [ ("core::fmt::Debug::Trait", []) ] ]
                          ]
                        |),
                        [ error ]
                      |)
                    ]
                |)
              ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_unwrap_failed : M.IsFunction "core::result::unwrap_failed" unwrap_failed.
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_T_where_core_clone_Clone_E_for_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    (*
        fn clone(&self) -> Self {
            match self {
                Ok(x) => Ok(x.clone()),
                Err(x) => Err(x.clone()),
            }
        }
    *)
    Definition clone (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 0 |) in
                    let x := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          M.call_closure (|
                            M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                            [ M.read (| x |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let x := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [
                          M.call_closure (|
                            M.get_trait_method (| "core::clone::Clone", E, [], "clone", [] |),
                            [ M.read (| x |) ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn clone_from(&mut self, source: &Self) {
            match (self, source) {
                (Ok(to), Ok(from)) => to.clone_from(from),
                (Err(to), Err(from)) => to.clone_from(from),
                (to, from) => *to = from.clone(),
            }
        }
    *)
    Definition clone_from (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self; source ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let source := M.alloc (| source |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [ M.read (| self |); M.read (| source |) ] |),
              [
                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::result::Result::Ok",
                        0
                      |) in
                    let to := 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::result::Result::Ok",
                        0
                      |) in
                    let from := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::clone::Clone", T, [], "clone_from", [] |),
                        [ M.read (| to |); M.read (| from |) ]
                      |)
                    |)));
                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::result::Result::Err",
                        0
                      |) in
                    let to := 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::result::Result::Err",
                        0
                      |) in
                    let from := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::clone::Clone", E, [], "clone_from", [] |),
                        [ M.read (| to |); M.read (| from |) ]
                      |)
                    |)));
                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 to := M.copy (| γ0_0 |) in
                    let from := M.copy (| γ0_1 |) in
                    M.write (|
                      M.read (| to |),
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::clone::Clone",
                          Ty.apply (Ty.path "core::result::Result") [] [ T; E ],
                          [],
                          "clone",
                          []
                        |),
                        [ M.read (| from |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T E : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("clone", InstanceField.Method (clone T E));
          ("clone_from", InstanceField.Method (clone_from T E))
        ].
  End Impl_core_clone_Clone_where_core_clone_Clone_T_where_core_clone_Clone_E_for_core_result_Result_T_E.
  
  Module Impl_core_iter_traits_collect_IntoIterator_for_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    (*     type Item = T; *)
    Definition _Item (T E : Ty.t) : Ty.t := T.
    
    (*     type IntoIter = IntoIter<T>; *)
    Definition _IntoIter (T E : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::result::IntoIter") [] [ T ].
    
    (*
        fn into_iter(self) -> IntoIter<T> {
            IntoIter { inner: self.ok() }
        }
    *)
    Definition into_iter (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::result::IntoIter"
            [
              ("inner",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::result::Result") [] [ T; E ],
                    "ok",
                    []
                  |),
                  [ M.read (| self |) ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T E : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::collect::IntoIterator"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item T E));
          ("IntoIter", InstanceField.Ty (_IntoIter T E));
          ("into_iter", InstanceField.Method (into_iter T E))
        ].
  End Impl_core_iter_traits_collect_IntoIterator_for_core_result_Result_T_E.
  
  Module Impl_core_iter_traits_collect_IntoIterator_for_ref__core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "core::result::Result") [] [ T; E ] ].
    
    (*     type Item = &'a T; *)
    Definition _Item (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    (*     type IntoIter = Iter<'a, T>; *)
    Definition _IntoIter (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Iter") [] [ T ].
    
    (*
        fn into_iter(self) -> Iter<'a, T> {
            self.iter()
        }
    *)
    Definition into_iter (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::result::Result") [] [ T; E ],
              "iter",
              []
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T E : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::collect::IntoIterator"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item T E));
          ("IntoIter", InstanceField.Ty (_IntoIter T E));
          ("into_iter", InstanceField.Method (into_iter T E))
        ].
  End Impl_core_iter_traits_collect_IntoIterator_for_ref__core_result_Result_T_E.
  
  Module Impl_core_iter_traits_collect_IntoIterator_for_ref_mut_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "core::result::Result") [] [ T; E ] ].
    
    (*     type Item = &'a mut T; *)
    Definition _Item (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
    
    (*     type IntoIter = IterMut<'a, T>; *)
    Definition _IntoIter (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IterMut") [] [ T ].
    
    (*
        fn into_iter(self) -> IterMut<'a, T> {
            self.iter_mut()
        }
    *)
    Definition into_iter (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::result::Result") [] [ T; E ],
              "iter_mut",
              []
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T E : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::collect::IntoIterator"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item T E));
          ("IntoIter", InstanceField.Ty (_IntoIter T E));
          ("into_iter", InstanceField.Method (into_iter T E))
        ].
  End Impl_core_iter_traits_collect_IntoIterator_for_ref_mut_core_result_Result_T_E.
  
  (* StructRecord
    {
      name := "Iter";
      const_params := [];
      ty_params := [ "T" ];
      fields :=
        [
          ("inner",
            Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&") [] [ T ] ])
        ];
    } *)
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_result_Iter_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Iter") [] [ T ].
    
    (* Debug *)
    Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "Iter" |);
              M.read (| Value.String "inner" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::result::Iter",
                  "inner"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_result_Iter_T.
  
  Module Impl_core_iter_traits_iterator_Iterator_for_core_result_Iter_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Iter") [] [ T ].
    
    (*     type Item = &'a T; *)
    Definition _Item (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    (*
        fn next(&mut self) -> Option<&'a T> {
            self.inner.take()
        }
    *)
    Definition next (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&") [] [ T ] ],
              "take",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::result::Iter",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn size_hint(&self) -> (usize, Option<usize>) {
            let n = if self.inner.is_some() { 1 } else { 0 };
            (n, Some(n))
        }
    *)
    Definition size_hint (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ n :=
              M.copy (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [ Ty.apply (Ty.path "&") [] [ T ] ],
                                  "is_some",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::result::Iter",
                                    "inner"
                                  |)
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.Integer IntegerKind.Usize 1 |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                  ]
                |)
              |) in
            M.alloc (|
              Value.Tuple
                [ M.read (| n |); Value.StructTuple "core::option::Option::Some" [ M.read (| n |) ]
                ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::iterator::Iterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item T));
          ("next", InstanceField.Method (next T));
          ("size_hint", InstanceField.Method (size_hint T))
        ].
  End Impl_core_iter_traits_iterator_Iterator_for_core_result_Iter_T.
  
  Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_result_Iter_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Iter") [] [ T ].
    
    (*
        fn next_back(&mut self) -> Option<&'a T> {
            self.inner.take()
        }
    *)
    Definition next_back (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&") [] [ T ] ],
              "take",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::result::Iter",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::double_ended::DoubleEndedIterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("next_back", InstanceField.Method (next_back T)) ].
  End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_result_Iter_T.
  
  Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_result_Iter_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Iter") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::exact_size::ExactSizeIterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_result_Iter_T.
  
  Module Impl_core_iter_traits_marker_FusedIterator_for_core_result_Iter_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Iter") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::FusedIterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_FusedIterator_for_core_result_Iter_T.
  
  Module Impl_core_iter_traits_marker_TrustedLen_for_core_result_Iter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Iter") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::TrustedLen"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_TrustedLen_for_core_result_Iter_A.
  
  Module Impl_core_clone_Clone_for_core_result_Iter_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Iter") [] [ T ].
    
    (*
        fn clone(&self) -> Self {
            Iter { inner: self.inner }
        }
    *)
    Definition clone (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::result::Iter"
            [
              ("inner",
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::result::Iter",
                    "inner"
                  |)
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone T)) ].
  End Impl_core_clone_Clone_for_core_result_Iter_T.
  
  (* StructRecord
    {
      name := "IterMut";
      const_params := [];
      ty_params := [ "T" ];
      fields :=
        [
          ("inner",
            Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&mut") [] [ T ] ])
        ];
    } *)
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_result_IterMut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IterMut") [] [ T ].
    
    (* Debug *)
    Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "IterMut" |);
              M.read (| Value.String "inner" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::result::IterMut",
                  "inner"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_result_IterMut_T.
  
  Module Impl_core_iter_traits_iterator_Iterator_for_core_result_IterMut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IterMut") [] [ T ].
    
    (*     type Item = &'a mut T; *)
    Definition _Item (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
    
    (*
        fn next(&mut self) -> Option<&'a mut T> {
            self.inner.take()
        }
    *)
    Definition next (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&mut") [] [ T ] ],
              "take",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::result::IterMut",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn size_hint(&self) -> (usize, Option<usize>) {
            let n = if self.inner.is_some() { 1 } else { 0 };
            (n, Some(n))
        }
    *)
    Definition size_hint (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ n :=
              M.copy (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                                  "is_some",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::result::IterMut",
                                    "inner"
                                  |)
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.Integer IntegerKind.Usize 1 |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                  ]
                |)
              |) in
            M.alloc (|
              Value.Tuple
                [ M.read (| n |); Value.StructTuple "core::option::Option::Some" [ M.read (| n |) ]
                ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::iterator::Iterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item T));
          ("next", InstanceField.Method (next T));
          ("size_hint", InstanceField.Method (size_hint T))
        ].
  End Impl_core_iter_traits_iterator_Iterator_for_core_result_IterMut_T.
  
  Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_result_IterMut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IterMut") [] [ T ].
    
    (*
        fn next_back(&mut self) -> Option<&'a mut T> {
            self.inner.take()
        }
    *)
    Definition next_back (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&mut") [] [ T ] ],
              "take",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::result::IterMut",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::double_ended::DoubleEndedIterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("next_back", InstanceField.Method (next_back T)) ].
  End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_result_IterMut_T.
  
  Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_result_IterMut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IterMut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::exact_size::ExactSizeIterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_result_IterMut_T.
  
  Module Impl_core_iter_traits_marker_FusedIterator_for_core_result_IterMut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IterMut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::FusedIterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_FusedIterator_for_core_result_IterMut_T.
  
  Module Impl_core_iter_traits_marker_TrustedLen_for_core_result_IterMut_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IterMut") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::TrustedLen"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_TrustedLen_for_core_result_IterMut_A.
  
  (* StructRecord
    {
      name := "IntoIter";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ ("inner", Ty.apply (Ty.path "core::option::Option") [] [ T ]) ];
    } *)
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_result_IntoIter_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IntoIter") [] [ T ].
    
    (* Clone *)
    Definition clone (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::result::IntoIter"
            [
              ("inner",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "core::option::Option") [] [ T ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::result::IntoIter",
                      "inner"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone T)) ].
  End Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_result_IntoIter_T.
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_result_IntoIter_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IntoIter") [] [ T ].
    
    (* Debug *)
    Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "IntoIter" |);
              M.read (| Value.String "inner" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::result::IntoIter",
                  "inner"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_result_IntoIter_T.
  
  Module Impl_core_iter_traits_iterator_Iterator_for_core_result_IntoIter_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IntoIter") [] [ T ].
    
    (*     type Item = T; *)
    Definition _Item (T : Ty.t) : Ty.t := T.
    
    (*
        fn next(&mut self) -> Option<T> {
            self.inner.take()
        }
    *)
    Definition next (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ T ],
              "take",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::result::IntoIter",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn size_hint(&self) -> (usize, Option<usize>) {
            let n = if self.inner.is_some() { 1 } else { 0 };
            (n, Some(n))
        }
    *)
    Definition size_hint (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ n :=
              M.copy (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "core::option::Option") [] [ T ],
                                  "is_some",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::result::IntoIter",
                                    "inner"
                                  |)
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.Integer IntegerKind.Usize 1 |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                  ]
                |)
              |) in
            M.alloc (|
              Value.Tuple
                [ M.read (| n |); Value.StructTuple "core::option::Option::Some" [ M.read (| n |) ]
                ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::iterator::Iterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item T));
          ("next", InstanceField.Method (next T));
          ("size_hint", InstanceField.Method (size_hint T))
        ].
  End Impl_core_iter_traits_iterator_Iterator_for_core_result_IntoIter_T.
  
  Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_result_IntoIter_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IntoIter") [] [ T ].
    
    (*
        fn next_back(&mut self) -> Option<T> {
            self.inner.take()
        }
    *)
    Definition next_back (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ T ],
              "take",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::result::IntoIter",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::double_ended::DoubleEndedIterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("next_back", InstanceField.Method (next_back T)) ].
  End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_result_IntoIter_T.
  
  Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_result_IntoIter_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IntoIter") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::exact_size::ExactSizeIterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_result_IntoIter_T.
  
  Module Impl_core_iter_traits_marker_FusedIterator_for_core_result_IntoIter_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IntoIter") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::FusedIterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_FusedIterator_for_core_result_IntoIter_T.
  
  Module Impl_core_iter_traits_marker_TrustedLen_for_core_result_IntoIter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::IntoIter") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::TrustedLen"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_TrustedLen_for_core_result_IntoIter_A.
  
  Module Impl_core_iter_traits_collect_FromIterator_where_core_iter_traits_collect_FromIterator_V_A_core_result_Result_A_E_for_core_result_Result_V_E.
    Definition Self (A E V : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ V; E ].
    
    (*
        fn from_iter<I: IntoIterator<Item = Result<A, E>>>(iter: I) -> Result<V, E> {
            iter::try_process(iter.into_iter(), |i| i.collect())
        }
    *)
    Definition from_iter (A E V : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A E V in
      match ε, τ, α with
      | [], [ _ as I ], [ iter ] =>
        ltac:(M.monadic
          (let iter := M.alloc (| iter |) in
          M.call_closure (|
            M.get_function (|
              "core::iter::adapters::try_process",
              [
                Ty.associated;
                A;
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [ Ty.path "core::convert::Infallible"; E ];
                Ty.function
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "core::iter::adapters::GenericShunt")
                          []
                          [
                            Ty.associated;
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [ Ty.path "core::convert::Infallible"; E ]
                          ]
                      ]
                  ]
                  V;
                V
              ]
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::collect::IntoIterator",
                  I,
                  [],
                  "into_iter",
                  []
                |),
                [ M.read (| iter |) ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let i := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    Ty.apply
                                      (Ty.path "core::iter::adapters::GenericShunt")
                                      []
                                      [
                                        Ty.associated;
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [ Ty.path "core::convert::Infallible"; E ]
                                      ],
                                    [],
                                    "collect",
                                    [ V ]
                                  |),
                                  [ M.read (| i |) ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A E V : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::collect::FromIterator"
        (Self A E V)
        (* Trait polymorphic types *)
        [ (* A *) Ty.apply (Ty.path "core::result::Result") [] [ A; E ] ]
        (* Instance *) [ ("from_iter", InstanceField.Method (from_iter A E V)) ].
  End Impl_core_iter_traits_collect_FromIterator_where_core_iter_traits_collect_FromIterator_V_A_core_result_Result_A_E_for_core_result_Result_V_E.
  
  Module Impl_core_ops_try_trait_Try_for_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    (*     type Output = T; *)
    Definition _Output (T E : Ty.t) : Ty.t := T.
    
    (*     type Residual = Result<convert::Infallible, E>; *)
    Definition _Residual (T E : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::result::Result") [] [ Ty.path "core::convert::Infallible"; E ].
    
    (*
        fn from_output(output: Self::Output) -> Self {
            Ok(output)
        }
    *)
    Definition from_output (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ output ] =>
        ltac:(M.monadic
          (let output := M.alloc (| output |) in
          Value.StructTuple "core::result::Result::Ok" [ M.read (| output |) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn branch(self) -> ControlFlow<Self::Residual, Self::Output> {
            match self {
                Ok(v) => ControlFlow::Continue(v),
                Err(e) => ControlFlow::Break(Err(e)),
            }
        }
    *)
    Definition branch (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E 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::result::Result::Ok", 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::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::ops::control_flow::ControlFlow::Break"
                        [ Value.StructTuple "core::result::Result::Err" [ M.read (| e |) ] ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T E : Ty.t),
      M.IsTraitInstance
        "core::ops::try_trait::Try"
        (Self T E)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Output", InstanceField.Ty (_Output T E));
          ("Residual", InstanceField.Ty (_Residual T E));
          ("from_output", InstanceField.Method (from_output T E));
          ("branch", InstanceField.Method (branch T E))
        ].
  End Impl_core_ops_try_trait_Try_for_core_result_Result_T_E.
  
  Module Impl_core_ops_try_trait_FromResidual_where_core_convert_From_F_E_core_result_Result_core_convert_Infallible_E_for_core_result_Result_T_F.
    Definition Self (T E F : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; F ].
    
    (*
        fn from_residual(residual: Result<convert::Infallible, E>) -> Self {
            match residual {
                Err(e) => Err(From::from(e)),
            }
        }
    *)
    Definition from_residual
        (T E F : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T E F 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::result::Result::Err", 0 |) in
                    let e := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [
                          M.call_closure (|
                            M.get_trait_method (| "core::convert::From", F, [ E ], "from", [] |),
                            [ M.read (| e |) ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T E F : Ty.t),
      M.IsTraitInstance
        "core::ops::try_trait::FromResidual"
        (Self T E F)
        (* Trait polymorphic types *)
        [
          (* R *)
          Ty.apply (Ty.path "core::result::Result") [] [ Ty.path "core::convert::Infallible"; E ]
        ]
        (* Instance *) [ ("from_residual", InstanceField.Method (from_residual T E F)) ].
  End Impl_core_ops_try_trait_FromResidual_where_core_convert_From_F_E_core_result_Result_core_convert_Infallible_E_for_core_result_Result_T_F.
  
  Module Impl_core_ops_try_trait_FromResidual_where_core_convert_From_F_E_core_ops_try_trait_Yeet_E_for_core_result_Result_T_F.
    Definition Self (T E F : Ty.t) : Ty.t := Ty.apply (Ty.path "core::result::Result") [] [ T; F ].
    
    (*
        fn from_residual(ops::Yeet(e): ops::Yeet<E>) -> Self {
            Err(From::from(e))
        }
    *)
    Definition from_residual
        (T E F : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T E F in
      match ε, τ, α with
      | [], [], [ β0 ] =>
        ltac:(M.monadic
          (let β0 := M.alloc (| β0 |) in
          M.match_operator (|
            β0,
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::ops::try_trait::Yeet", 0 |) in
                  let e := M.copy (| γ0_0 |) in
                  Value.StructTuple
                    "core::result::Result::Err"
                    [
                      M.call_closure (|
                        M.get_trait_method (| "core::convert::From", F, [ E ], "from", [] |),
                        [ M.read (| e |) ]
                      |)
                    ]))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T E F : Ty.t),
      M.IsTraitInstance
        "core::ops::try_trait::FromResidual"
        (Self T E F)
        (* Trait polymorphic types *)
        [ (* R *) Ty.apply (Ty.path "core::ops::try_trait::Yeet") [] [ E ] ]
        (* Instance *) [ ("from_residual", InstanceField.Method (from_residual T E F)) ].
  End Impl_core_ops_try_trait_FromResidual_where_core_convert_From_F_E_core_ops_try_trait_Yeet_E_for_core_result_Result_T_F.
  
  Module Impl_core_ops_try_trait_Residual_T_for_core_result_Result_core_convert_Infallible_E.
    Definition Self (T E : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::result::Result") [] [ Ty.path "core::convert::Infallible"; E ].
    
    (*     type TryType = Result<T, E>; *)
    Definition _TryType (T E : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::result::Result") [] [ T; E ].
    
    Axiom Implements :
      forall (T E : Ty.t),
      M.IsTraitInstance
        "core::ops::try_trait::Residual"
        (Self T E)
        (* Trait polymorphic types *) [ (* O *) T ]
        (* Instance *) [ ("TryType", InstanceField.Ty (_TryType T E)) ].
  End Impl_core_ops_try_trait_Residual_T_for_core_result_Result_core_convert_Infallible_E.
End result.
