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

Module num.
  Module error.
    (* StructTuple
      {
        name := "TryFromIntError";
        const_params := [];
        ty_params := [];
        fields := [ Ty.tuple [] ];
      } *)
    
    Module Impl_core_fmt_Debug_for_core_num_error_TryFromIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::TryFromIntError".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        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_tuple_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "TryFromIntError" |);
                M.alloc (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "core::num::error::TryFromIntError",
                    0
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_num_error_TryFromIntError.
    
    Module Impl_core_marker_Copy_for_core_num_error_TryFromIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::TryFromIntError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_num_error_TryFromIntError.
    
    Module Impl_core_clone_Clone_for_core_num_error_TryFromIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::TryFromIntError".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_num_error_TryFromIntError.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_num_error_TryFromIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::TryFromIntError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_num_error_TryFromIntError.
    
    Module Impl_core_cmp_PartialEq_for_core_num_error_TryFromIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::TryFromIntError".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.tuple [],
                [ Ty.tuple [] ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "core::num::error::TryFromIntError",
                  0
                |);
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| other |),
                  "core::num::error::TryFromIntError",
                  0
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_num_error_TryFromIntError.
    
    Module Impl_core_cmp_Eq_for_core_num_error_TryFromIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::TryFromIntError".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_num_error_TryFromIntError.
    
    Module Impl_core_fmt_Display_for_core_num_error_TryFromIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::TryFromIntError".
      
      (*
          fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
              #[allow(deprecated)]
              self.description().fmt(fmt)
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; fmt ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let fmt := M.alloc (| fmt |) in
            M.call_closure (|
              M.get_trait_method (| "core::fmt::Display", Ty.path "str", [], "fmt", [] |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::error::Error",
                    Ty.path "core::num::error::TryFromIntError",
                    [],
                    "description",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| fmt |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Display"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Display_for_core_num_error_TryFromIntError.
    
    Module Impl_core_error_Error_for_core_num_error_TryFromIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::TryFromIntError".
      
      (*
          fn description(&self) -> &str {
              "out of range integral type conversion attempted"
          }
      *)
      Definition description (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| Value.String "out of range integral type conversion attempted" |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::error::Error"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("description", InstanceField.Method description) ].
    End Impl_core_error_Error_for_core_num_error_TryFromIntError.
    
    Module Impl_core_convert_From_core_convert_Infallible_for_core_num_error_TryFromIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::TryFromIntError".
      
      (*
          fn from(x: Infallible) -> TryFromIntError {
              match x {}
          }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ x ] =>
          ltac:(M.monadic
            (let x := M.alloc (| x |) in
            M.never_to_any (| M.read (| M.match_operator (| x, [] |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "core::convert::Infallible" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_core_convert_Infallible_for_core_num_error_TryFromIntError.
    
    Module Impl_core_convert_From_never_for_core_num_error_TryFromIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::TryFromIntError".
      
      (*
          fn from(never: !) -> TryFromIntError {
              // Match rather than coerce to make sure that code like
              // `From<Infallible> for TryFromIntError` above will keep working
              // when `Infallible` becomes an alias to `!`.
              match never {}
          }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ never ] =>
          ltac:(M.monadic
            (let never := M.alloc (| never |) in
            M.never_to_any (| M.read (| M.match_operator (| never, [] |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "never" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_never_for_core_num_error_TryFromIntError.
    
    (* StructRecord
      {
        name := "ParseIntError";
        const_params := [];
        ty_params := [];
        fields := [ ("kind", Ty.path "core::num::error::IntErrorKind") ];
      } *)
    
    Module Impl_core_fmt_Debug_for_core_num_error_ParseIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::ParseIntError".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        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 "ParseIntError" |);
                M.read (| Value.String "kind" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::num::error::ParseIntError",
                    "kind"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_num_error_ParseIntError.
    
    Module Impl_core_clone_Clone_for_core_num_error_ParseIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::ParseIntError".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "core::num::error::ParseIntError"
              [
                ("kind",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "core::num::error::IntErrorKind",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::num::error::ParseIntError",
                        "kind"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_num_error_ParseIntError.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_num_error_ParseIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::ParseIntError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_num_error_ParseIntError.
    
    Module Impl_core_cmp_PartialEq_for_core_num_error_ParseIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::ParseIntError".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.path "core::num::error::IntErrorKind",
                [ Ty.path "core::num::error::IntErrorKind" ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::num::error::ParseIntError",
                  "kind"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "core::num::error::ParseIntError",
                  "kind"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_num_error_ParseIntError.
    
    Module Impl_core_cmp_Eq_for_core_num_error_ParseIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::ParseIntError".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_num_error_ParseIntError.
    
    (*
    Enum IntErrorKind
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Empty";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "InvalidDigit";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "PosOverflow";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "NegOverflow";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Zero";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_fmt_Debug_for_core_num_error_IntErrorKind.
      Definition Self : Ty.t := Ty.path "core::num::error::IntErrorKind".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        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", "write_str", [] |),
              [
                M.read (| f |);
                M.read (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (| γ, "core::num::error::IntErrorKind::Empty" |) in
                          M.alloc (| M.read (| Value.String "Empty" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "core::num::error::IntErrorKind::InvalidDigit"
                            |) in
                          M.alloc (| M.read (| Value.String "InvalidDigit" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "core::num::error::IntErrorKind::PosOverflow"
                            |) in
                          M.alloc (| M.read (| Value.String "PosOverflow" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "core::num::error::IntErrorKind::NegOverflow"
                            |) in
                          M.alloc (| M.read (| Value.String "NegOverflow" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (| γ, "core::num::error::IntErrorKind::Zero" |) in
                          M.alloc (| M.read (| Value.String "Zero" |) |)))
                    ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_num_error_IntErrorKind.
    
    Module Impl_core_clone_Clone_for_core_num_error_IntErrorKind.
      Definition Self : Ty.t := Ty.path "core::num::error::IntErrorKind".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        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 _ := M.is_struct_tuple (| γ, "core::num::error::IntErrorKind::Empty" |) in
                      M.alloc (| Value.StructTuple "core::num::error::IntErrorKind::Empty" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "core::num::error::IntErrorKind::InvalidDigit" |) in
                      M.alloc (|
                        Value.StructTuple "core::num::error::IntErrorKind::InvalidDigit" []
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "core::num::error::IntErrorKind::PosOverflow" |) in
                      M.alloc (|
                        Value.StructTuple "core::num::error::IntErrorKind::PosOverflow" []
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "core::num::error::IntErrorKind::NegOverflow" |) in
                      M.alloc (|
                        Value.StructTuple "core::num::error::IntErrorKind::NegOverflow" []
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ := M.is_struct_tuple (| γ, "core::num::error::IntErrorKind::Zero" |) in
                      M.alloc (| Value.StructTuple "core::num::error::IntErrorKind::Zero" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_num_error_IntErrorKind.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_num_error_IntErrorKind.
      Definition Self : Ty.t := Ty.path "core::num::error::IntErrorKind".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_num_error_IntErrorKind.
    
    Module Impl_core_cmp_PartialEq_for_core_num_error_IntErrorKind.
      Definition Self : Ty.t := Ty.path "core::num::error::IntErrorKind".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        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.path "core::num::error::IntErrorKind" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::num::error::IntErrorKind" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_num_error_IntErrorKind.
    
    Module Impl_core_cmp_Eq_for_core_num_error_IntErrorKind.
      Definition Self : Ty.t := Ty.path "core::num::error::IntErrorKind".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.Tuple []))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_num_error_IntErrorKind.
    
    Module Impl_core_num_error_ParseIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::ParseIntError".
      
      (*
          pub const fn kind(&self) -> &IntErrorKind {
              &self.kind
          }
      *)
      Definition kind (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "core::num::error::ParseIntError",
              "kind"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_kind : M.IsAssociatedFunction Self "kind" kind.
    End Impl_core_num_error_ParseIntError.
    
    Module Impl_core_fmt_Display_for_core_num_error_ParseIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::ParseIntError".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              #[allow(deprecated)]
              self.description().fmt(f)
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_trait_method (| "core::fmt::Display", Ty.path "str", [], "fmt", [] |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::error::Error",
                    Ty.path "core::num::error::ParseIntError",
                    [],
                    "description",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| f |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Display"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Display_for_core_num_error_ParseIntError.
    
    Module Impl_core_error_Error_for_core_num_error_ParseIntError.
      Definition Self : Ty.t := Ty.path "core::num::error::ParseIntError".
      
      (*
          fn description(&self) -> &str {
              match self.kind {
                  IntErrorKind::Empty => "cannot parse integer from empty string",
                  IntErrorKind::InvalidDigit => "invalid digit found in string",
                  IntErrorKind::PosOverflow => "number too large to fit in target type",
                  IntErrorKind::NegOverflow => "number too small to fit in target type",
                  IntErrorKind::Zero => "number would be zero for non-zero type",
              }
          }
      *)
      Definition description (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::num::error::ParseIntError",
                  "kind"
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (| γ, "core::num::error::IntErrorKind::Empty" |) in
                      M.alloc (|
                        M.read (| Value.String "cannot parse integer from empty string" |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (| γ, "core::num::error::IntErrorKind::InvalidDigit" |) in
                      M.alloc (| M.read (| Value.String "invalid digit found in string" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (| γ, "core::num::error::IntErrorKind::PosOverflow" |) in
                      M.alloc (|
                        M.read (| Value.String "number too large to fit in target type" |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (| γ, "core::num::error::IntErrorKind::NegOverflow" |) in
                      M.alloc (|
                        M.read (| Value.String "number too small to fit in target type" |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::num::error::IntErrorKind::Zero" |) in
                      M.alloc (|
                        M.read (| Value.String "number would be zero for non-zero type" |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::error::Error"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("description", InstanceField.Method description) ].
    End Impl_core_error_Error_for_core_num_error_ParseIntError.
  End error.
End num.
