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

Module str.
  Module error.
    (* StructRecord
      {
        name := "Utf8Error";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("valid_up_to", Ty.path "usize");
            ("error_len", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u8" ])
          ];
      } *)
    
    Module Impl_core_marker_Copy_for_core_str_error_Utf8Error.
      Definition Self : Ty.t := Ty.path "core::str::error::Utf8Error".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_str_error_Utf8Error.
    
    Module Impl_core_cmp_Eq_for_core_str_error_Utf8Error.
      Definition Self : Ty.t := Ty.path "core::str::error::Utf8Error".
      
      (* 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.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_str_error_Utf8Error.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_str_error_Utf8Error.
      Definition Self : Ty.t := Ty.path "core::str::error::Utf8Error".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_str_error_Utf8Error.
    
    Module Impl_core_cmp_PartialEq_for_core_str_error_Utf8Error.
      Definition Self : Ty.t := Ty.path "core::str::error::Utf8Error".
      
      (* 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
            LogicalOp.and (|
              BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::str::error::Utf8Error",
                    "valid_up_to"
                  |)
                |),
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "core::str::error::Utf8Error",
                    "valid_up_to"
                  |)
                |)
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u8" ],
                    [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u8" ] ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::str::error::Utf8Error",
                      "error_len"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "core::str::error::Utf8Error",
                      "error_len"
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => 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_str_error_Utf8Error.
    
    Module Impl_core_clone_Clone_for_core_str_error_Utf8Error.
      Definition Self : Ty.t := Ty.path "core::str::error::Utf8Error".
      
      (* 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.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_str_error_Utf8Error.
    
    Module Impl_core_fmt_Debug_for_core_str_error_Utf8Error.
      Definition Self : Ty.t := Ty.path "core::str::error::Utf8Error".
      
      (* 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_field2_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "Utf8Error" |);
                M.read (| Value.String "valid_up_to" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::str::error::Utf8Error",
                  "valid_up_to"
                |);
                M.read (| Value.String "error_len" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::str::error::Utf8Error",
                    "error_len"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_str_error_Utf8Error.
    
    Module Impl_core_str_error_Utf8Error.
      Definition Self : Ty.t := Ty.path "core::str::error::Utf8Error".
      
      (*
          pub const fn valid_up_to(&self) -> usize {
              self.valid_up_to
          }
      *)
      Definition valid_up_to (ε : 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.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::str::error::Utf8Error",
                "valid_up_to"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_valid_up_to : M.IsAssociatedFunction Self "valid_up_to" valid_up_to.
      
      (*
          pub const fn error_len(&self) -> Option<usize> {
              // FIXME(const-hack): This should become `map` again, once it's `const`
              match self.error_len {
                  Some(len) => Some(len as usize),
                  None => None,
              }
          }
      *)
      Definition error_len (ε : 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::str::error::Utf8Error",
                  "error_len"
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let len := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ M.rust_cast (M.read (| len |)) ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_error_len : M.IsAssociatedFunction Self "error_len" error_len.
    End Impl_core_str_error_Utf8Error.
    
    Module Impl_core_fmt_Display_for_core_str_error_Utf8Error.
      Definition Self : Ty.t := Ty.path "core::str::error::Utf8Error".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              if let Some(error_len) = self.error_len {
                  write!(
                      f,
                      "invalid utf-8 sequence of {} bytes from index {}",
                      error_len, self.valid_up_to
                  )
              } else {
                  write!(f, "incomplete utf-8 byte sequence from index {}", self.valid_up_to)
              }
          }
      *)
      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.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::str::error::Utf8Error",
                          "error_len"
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let error_len := M.copy (| γ0_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "write_fmt",
                            []
                          |),
                          [
                            M.read (| f |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Arguments",
                                "new_v1",
                                []
                              |),
                              [
                                M.alloc (|
                                  Value.Array
                                    [
                                      M.read (| Value.String "invalid utf-8 sequence of " |);
                                      M.read (| Value.String " bytes from index " |)
                                    ]
                                |);
                                M.alloc (|
                                  Value.Array
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [ Ty.path "u8" ]
                                        |),
                                        [ error_len ]
                                      |);
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [ Ty.path "usize" ]
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::str::error::Utf8Error",
                                            "valid_up_to"
                                          |)
                                        ]
                                      |)
                                    ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "write_fmt",
                            []
                          |),
                          [
                            M.read (| f |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Arguments",
                                "new_v1",
                                []
                              |),
                              [
                                M.alloc (|
                                  Value.Array
                                    [
                                      M.read (|
                                        Value.String "incomplete utf-8 byte sequence from index "
                                      |)
                                    ]
                                |);
                                M.alloc (|
                                  Value.Array
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::rt::Argument",
                                          "new_display",
                                          [ Ty.path "usize" ]
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::str::error::Utf8Error",
                                            "valid_up_to"
                                          |)
                                        ]
                                      |)
                                    ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => 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_str_error_Utf8Error.
    
    Module Impl_core_error_Error_for_core_str_error_Utf8Error.
      Definition Self : Ty.t := Ty.path "core::str::error::Utf8Error".
      
      (*
          fn description(&self) -> &str {
              "invalid utf-8: corrupt contents"
          }
      *)
      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 "invalid utf-8: corrupt contents" |)))
        | _, _, _ => 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_str_error_Utf8Error.
    
    (* StructTuple
      {
        name := "ParseBoolError";
        const_params := [];
        ty_params := [];
        fields := [];
      } *)
    
    Module Impl_core_fmt_Debug_for_core_str_error_ParseBoolError.
      Definition Self : Ty.t := Ty.path "core::str::error::ParseBoolError".
      
      (* 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 (| Value.String "ParseBoolError" |) ]
            |)))
        | _, _, _ => 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_str_error_ParseBoolError.
    
    Module Impl_core_clone_Clone_for_core_str_error_ParseBoolError.
      Definition Self : Ty.t := Ty.path "core::str::error::ParseBoolError".
      
      (* 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.StructTuple "core::str::error::ParseBoolError" []))
        | _, _, _ => 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_str_error_ParseBoolError.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_str_error_ParseBoolError.
      Definition Self : Ty.t := Ty.path "core::str::error::ParseBoolError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_str_error_ParseBoolError.
    
    Module Impl_core_cmp_PartialEq_for_core_str_error_ParseBoolError.
      Definition Self : Ty.t := Ty.path "core::str::error::ParseBoolError".
      
      (* 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
            Value.Bool true))
        | _, _, _ => 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_str_error_ParseBoolError.
    
    Module Impl_core_cmp_Eq_for_core_str_error_ParseBoolError.
      Definition Self : Ty.t := Ty.path "core::str::error::ParseBoolError".
      
      (* 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_str_error_ParseBoolError.
    
    Module Impl_core_fmt_Display_for_core_str_error_ParseBoolError.
      Definition Self : Ty.t := Ty.path "core::str::error::ParseBoolError".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              "provided string was not `true` or `false`".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.read (| Value.String "provided string was not `true` or `false`" |);
                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_str_error_ParseBoolError.
    
    Module Impl_core_error_Error_for_core_str_error_ParseBoolError.
      Definition Self : Ty.t := Ty.path "core::str::error::ParseBoolError".
      
      (*
          fn description(&self) -> &str {
              "failed to parse bool"
          }
      *)
      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 "failed to parse bool" |)))
        | _, _, _ => 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_str_error_ParseBoolError.
  End error.
End str.
