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

Module str.
  Module lossy.
    Module Impl_slice_u8.
      Definition Self : Ty.t := Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ].
      
      (*
          pub fn utf8_chunks(&self) -> Utf8Chunks<'_> {
              Utf8Chunks { source: self }
          }
      *)
      Definition utf8_chunks (ε : 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::str::lossy::Utf8Chunks" [ ("source", M.read (| self |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_utf8_chunks : M.IsAssociatedFunction Self "utf8_chunks" utf8_chunks.
    End Impl_slice_u8.
    
    (* StructRecord
      {
        name := "Utf8Chunk";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("valid", Ty.apply (Ty.path "&") [] [ Ty.path "str" ]);
            ("invalid",
              Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ])
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_core_str_lossy_Utf8Chunk.
      Definition Self : Ty.t := Ty.path "core::str::lossy::Utf8Chunk".
      
      (* 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::str::lossy::Utf8Chunk"
              [
                ("valid",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply (Ty.path "&") [] [ Ty.path "str" ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::str::lossy::Utf8Chunk",
                        "valid"
                      |)
                    ]
                  |));
                ("invalid",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::str::lossy::Utf8Chunk",
                        "invalid"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_lossy_Utf8Chunk.
    
    Module Impl_core_fmt_Debug_for_core_str_lossy_Utf8Chunk.
      Definition Self : Ty.t := Ty.path "core::str::lossy::Utf8Chunk".
      
      (* 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 "Utf8Chunk" |);
                M.read (| Value.String "valid" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::str::lossy::Utf8Chunk",
                  "valid"
                |);
                M.read (| Value.String "invalid" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::str::lossy::Utf8Chunk",
                    "invalid"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_lossy_Utf8Chunk.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_str_lossy_Utf8Chunk.
      Definition Self : Ty.t := Ty.path "core::str::lossy::Utf8Chunk".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_str_lossy_Utf8Chunk.
    
    Module Impl_core_cmp_PartialEq_for_core_str_lossy_Utf8Chunk.
      Definition Self : Ty.t := Ty.path "core::str::lossy::Utf8Chunk".
      
      (* 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 (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply (Ty.path "&") [] [ Ty.path "str" ],
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::str::lossy::Utf8Chunk",
                    "valid"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "core::str::lossy::Utf8Chunk",
                    "valid"
                  |)
                ]
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                    [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                    ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::str::lossy::Utf8Chunk",
                      "invalid"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "core::str::lossy::Utf8Chunk",
                      "invalid"
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => 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_lossy_Utf8Chunk.
    
    Module Impl_core_cmp_Eq_for_core_str_lossy_Utf8Chunk.
      Definition Self : Ty.t := Ty.path "core::str::lossy::Utf8Chunk".
      
      (* 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_lossy_Utf8Chunk.
    
    Module Impl_core_str_lossy_Utf8Chunk.
      Definition Self : Ty.t := Ty.path "core::str::lossy::Utf8Chunk".
      
      (*
          pub fn valid(&self) -> &'a str {
              self.valid
          }
      *)
      Definition valid (ε : 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::lossy::Utf8Chunk",
                "valid"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_valid : M.IsAssociatedFunction Self "valid" valid.
      
      (*
          pub fn invalid(&self) -> &'a [u8] {
              self.invalid
          }
      *)
      Definition invalid (ε : 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::lossy::Utf8Chunk",
                "invalid"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_invalid : M.IsAssociatedFunction Self "invalid" invalid.
    End Impl_core_str_lossy_Utf8Chunk.
    
    (* StructTuple
      {
        name := "Debug";
        const_params := [];
        ty_params := [];
        fields := [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] ];
      } *)
    
    Module Impl_core_fmt_Debug_for_core_str_lossy_Debug.
      Definition Self : Ty.t := Ty.path "core::str::lossy::Debug".
      
      (*
          fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
              f.write_char('"')?;
      
              for chunk in self.0.utf8_chunks() {
                  // Valid part.
                  // Here we partially parse UTF-8 again which is suboptimal.
                  {
                      let valid = chunk.valid();
                      let mut from = 0;
                      for (i, c) in valid.char_indices() {
                          let esc = c.escape_debug();
                          // If char needs escaping, flush backlog so far and write, else skip
                          if esc.len() != 1 {
                              f.write_str(&valid[from..i])?;
                              for c in esc {
                                  f.write_char(c)?;
                              }
                              from = i + c.len_utf8();
                          }
                      }
                      f.write_str(&valid[from..])?;
                  }
      
                  // Broken parts of string as hex escape.
                  for &b in chunk.invalid() {
                      write!(f, "\\x{:02X}", b)?;
                  }
              }
      
              f.write_char('"')
          }
      *)
      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.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::fmt::Write",
                                Ty.path "core::fmt::Formatter",
                                [],
                                "write_char",
                                []
                              |),
                              [ M.read (| f |); Value.UnicodeChar 34 ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "core::fmt::Error"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |) in
                  let~ _ :=
                    M.use
                      (M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::collect::IntoIterator",
                              Ty.path "core::str::lossy::Utf8Chunks",
                              [],
                              "into_iter",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                  "utf8_chunks",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_tuple_field (|
                                      M.read (| self |),
                                      "core::str::lossy::Debug",
                                      0
                                    |)
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let iter := M.copy (| γ |) in
                              M.loop (|
                                ltac:(M.monadic
                                  (let~ _ :=
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.path "core::str::lossy::Utf8Chunks",
                                            [],
                                            "next",
                                            []
                                          |),
                                          [ iter ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "core::option::Option::None"
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (| M.read (| M.break (||) |) |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::option::Option::Some",
                                                0
                                              |) in
                                            let chunk := M.copy (| γ0_0 |) in
                                            let~ _ :=
                                              let~ valid :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "core::str::lossy::Utf8Chunk",
                                                      "valid",
                                                      []
                                                    |),
                                                    [ chunk ]
                                                  |)
                                                |) in
                                              let~ from :=
                                                M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                                              let~ _ :=
                                                M.use
                                                  (M.match_operator (|
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::iter::traits::collect::IntoIterator",
                                                          Ty.path "core::str::iter::CharIndices",
                                                          [],
                                                          "into_iter",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "str",
                                                              "char_indices",
                                                              []
                                                            |),
                                                            [ M.read (| valid |) ]
                                                          |)
                                                        ]
                                                      |)
                                                    |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let iter := M.copy (| γ |) in
                                                          M.loop (|
                                                            ltac:(M.monadic
                                                              (let~ _ :=
                                                                M.match_operator (|
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::iter::traits::iterator::Iterator",
                                                                        Ty.path
                                                                          "core::str::iter::CharIndices",
                                                                        [],
                                                                        "next",
                                                                        []
                                                                      |),
                                                                      [ iter ]
                                                                    |)
                                                                  |),
                                                                  [
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let _ :=
                                                                          M.is_struct_tuple (|
                                                                            γ,
                                                                            "core::option::Option::None"
                                                                          |) in
                                                                        M.alloc (|
                                                                          M.never_to_any (|
                                                                            M.read (|
                                                                              M.break (||)
                                                                            |)
                                                                          |)
                                                                        |)));
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let γ0_0 :=
                                                                          M.SubPointer.get_struct_tuple_field (|
                                                                            γ,
                                                                            "core::option::Option::Some",
                                                                            0
                                                                          |) in
                                                                        let γ1_0 :=
                                                                          M.SubPointer.get_tuple_field (|
                                                                            γ0_0,
                                                                            0
                                                                          |) in
                                                                        let γ1_1 :=
                                                                          M.SubPointer.get_tuple_field (|
                                                                            γ0_0,
                                                                            1
                                                                          |) in
                                                                        let i :=
                                                                          M.copy (| γ1_0 |) in
                                                                        let c :=
                                                                          M.copy (| γ1_1 |) in
                                                                        let~ esc :=
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path "char",
                                                                                "escape_debug",
                                                                                []
                                                                              |),
                                                                              [ M.read (| c |) ]
                                                                            |)
                                                                          |) in
                                                                        M.match_operator (|
                                                                          M.alloc (|
                                                                            Value.Tuple []
                                                                          |),
                                                                          [
                                                                            fun γ =>
                                                                              ltac:(M.monadic
                                                                                (let γ :=
                                                                                  M.use
                                                                                    (M.alloc (|
                                                                                      BinOp.ne (|
                                                                                        M.call_closure (|
                                                                                          M.get_trait_method (|
                                                                                            "core::iter::traits::exact_size::ExactSizeIterator",
                                                                                            Ty.path
                                                                                              "core::char::EscapeDebug",
                                                                                            [],
                                                                                            "len",
                                                                                            []
                                                                                          |),
                                                                                          [ esc ]
                                                                                        |),
                                                                                        Value.Integer
                                                                                          IntegerKind.Usize
                                                                                          1
                                                                                      |)
                                                                                    |)) in
                                                                                let _ :=
                                                                                  M.is_constant_or_break_match (|
                                                                                    M.read (| γ |),
                                                                                    Value.Bool true
                                                                                  |) in
                                                                                let~ _ :=
                                                                                  M.match_operator (|
                                                                                    M.alloc (|
                                                                                      M.call_closure (|
                                                                                        M.get_trait_method (|
                                                                                          "core::ops::try_trait::Try",
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "core::result::Result")
                                                                                            []
                                                                                            [
                                                                                              Ty.tuple
                                                                                                [];
                                                                                              Ty.path
                                                                                                "core::fmt::Error"
                                                                                            ],
                                                                                          [],
                                                                                          "branch",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.call_closure (|
                                                                                            M.get_associated_function (|
                                                                                              Ty.path
                                                                                                "core::fmt::Formatter",
                                                                                              "write_str",
                                                                                              []
                                                                                            |),
                                                                                            [
                                                                                              M.read (|
                                                                                                f
                                                                                              |);
                                                                                              M.call_closure (|
                                                                                                M.get_trait_method (|
                                                                                                  "core::ops::index::Index",
                                                                                                  Ty.path
                                                                                                    "str",
                                                                                                  [
                                                                                                    Ty.apply
                                                                                                      (Ty.path
                                                                                                        "core::ops::range::Range")
                                                                                                      []
                                                                                                      [
                                                                                                        Ty.path
                                                                                                          "usize"
                                                                                                      ]
                                                                                                  ],
                                                                                                  "index",
                                                                                                  []
                                                                                                |),
                                                                                                [
                                                                                                  M.read (|
                                                                                                    valid
                                                                                                  |);
                                                                                                  Value.StructRecord
                                                                                                    "core::ops::range::Range"
                                                                                                    [
                                                                                                      ("start",
                                                                                                        M.read (|
                                                                                                          from
                                                                                                        |));
                                                                                                      ("end_",
                                                                                                        M.read (|
                                                                                                          i
                                                                                                        |))
                                                                                                    ]
                                                                                                ]
                                                                                              |)
                                                                                            ]
                                                                                          |)
                                                                                        ]
                                                                                      |)
                                                                                    |),
                                                                                    [
                                                                                      fun γ =>
                                                                                        ltac:(M.monadic
                                                                                          (let
                                                                                                γ0_0 :=
                                                                                            M.SubPointer.get_struct_tuple_field (|
                                                                                              γ,
                                                                                              "core::ops::control_flow::ControlFlow::Break",
                                                                                              0
                                                                                            |) in
                                                                                          let
                                                                                                residual :=
                                                                                            M.copy (|
                                                                                              γ0_0
                                                                                            |) in
                                                                                          M.alloc (|
                                                                                            M.never_to_any (|
                                                                                              M.read (|
                                                                                                M.return_ (|
                                                                                                  M.call_closure (|
                                                                                                    M.get_trait_method (|
                                                                                                      "core::ops::try_trait::FromResidual",
                                                                                                      Ty.apply
                                                                                                        (Ty.path
                                                                                                          "core::result::Result")
                                                                                                        []
                                                                                                        [
                                                                                                          Ty.tuple
                                                                                                            [];
                                                                                                          Ty.path
                                                                                                            "core::fmt::Error"
                                                                                                        ],
                                                                                                      [
                                                                                                        Ty.apply
                                                                                                          (Ty.path
                                                                                                            "core::result::Result")
                                                                                                          []
                                                                                                          [
                                                                                                            Ty.path
                                                                                                              "core::convert::Infallible";
                                                                                                            Ty.path
                                                                                                              "core::fmt::Error"
                                                                                                          ]
                                                                                                      ],
                                                                                                      "from_residual",
                                                                                                      []
                                                                                                    |),
                                                                                                    [
                                                                                                      M.read (|
                                                                                                        residual
                                                                                                      |)
                                                                                                    ]
                                                                                                  |)
                                                                                                |)
                                                                                              |)
                                                                                            |)
                                                                                          |)));
                                                                                      fun γ =>
                                                                                        ltac:(M.monadic
                                                                                          (let
                                                                                                γ0_0 :=
                                                                                            M.SubPointer.get_struct_tuple_field (|
                                                                                              γ,
                                                                                              "core::ops::control_flow::ControlFlow::Continue",
                                                                                              0
                                                                                            |) in
                                                                                          let val :=
                                                                                            M.copy (|
                                                                                              γ0_0
                                                                                            |) in
                                                                                          val))
                                                                                    ]
                                                                                  |) in
                                                                                let~ _ :=
                                                                                  M.use
                                                                                    (M.match_operator (|
                                                                                      M.alloc (|
                                                                                        M.call_closure (|
                                                                                          M.get_trait_method (|
                                                                                            "core::iter::traits::collect::IntoIterator",
                                                                                            Ty.path
                                                                                              "core::char::EscapeDebug",
                                                                                            [],
                                                                                            "into_iter",
                                                                                            []
                                                                                          |),
                                                                                          [
                                                                                            M.read (|
                                                                                              esc
                                                                                            |)
                                                                                          ]
                                                                                        |)
                                                                                      |),
                                                                                      [
                                                                                        fun γ =>
                                                                                          ltac:(M.monadic
                                                                                            (let
                                                                                                  iter :=
                                                                                              M.copy (|
                                                                                                γ
                                                                                              |) in
                                                                                            M.loop (|
                                                                                              ltac:(M.monadic
                                                                                                (let~
                                                                                                      _ :=
                                                                                                  M.match_operator (|
                                                                                                    M.alloc (|
                                                                                                      M.call_closure (|
                                                                                                        M.get_trait_method (|
                                                                                                          "core::iter::traits::iterator::Iterator",
                                                                                                          Ty.path
                                                                                                            "core::char::EscapeDebug",
                                                                                                          [],
                                                                                                          "next",
                                                                                                          []
                                                                                                        |),
                                                                                                        [
                                                                                                          iter
                                                                                                        ]
                                                                                                      |)
                                                                                                    |),
                                                                                                    [
                                                                                                      fun
                                                                                                          γ =>
                                                                                                        ltac:(M.monadic
                                                                                                          (let
                                                                                                                _ :=
                                                                                                            M.is_struct_tuple (|
                                                                                                              γ,
                                                                                                              "core::option::Option::None"
                                                                                                            |) in
                                                                                                          M.alloc (|
                                                                                                            M.never_to_any (|
                                                                                                              M.read (|
                                                                                                                M.break (||)
                                                                                                              |)
                                                                                                            |)
                                                                                                          |)));
                                                                                                      fun
                                                                                                          γ =>
                                                                                                        ltac:(M.monadic
                                                                                                          (let
                                                                                                                γ0_0 :=
                                                                                                            M.SubPointer.get_struct_tuple_field (|
                                                                                                              γ,
                                                                                                              "core::option::Option::Some",
                                                                                                              0
                                                                                                            |) in
                                                                                                          let
                                                                                                                c :=
                                                                                                            M.copy (|
                                                                                                              γ0_0
                                                                                                            |) in
                                                                                                          let~
                                                                                                                _ :=
                                                                                                            M.match_operator (|
                                                                                                              M.alloc (|
                                                                                                                M.call_closure (|
                                                                                                                  M.get_trait_method (|
                                                                                                                    "core::ops::try_trait::Try",
                                                                                                                    Ty.apply
                                                                                                                      (Ty.path
                                                                                                                        "core::result::Result")
                                                                                                                      []
                                                                                                                      [
                                                                                                                        Ty.tuple
                                                                                                                          [];
                                                                                                                        Ty.path
                                                                                                                          "core::fmt::Error"
                                                                                                                      ],
                                                                                                                    [],
                                                                                                                    "branch",
                                                                                                                    []
                                                                                                                  |),
                                                                                                                  [
                                                                                                                    M.call_closure (|
                                                                                                                      M.get_trait_method (|
                                                                                                                        "core::fmt::Write",
                                                                                                                        Ty.path
                                                                                                                          "core::fmt::Formatter",
                                                                                                                        [],
                                                                                                                        "write_char",
                                                                                                                        []
                                                                                                                      |),
                                                                                                                      [
                                                                                                                        M.read (|
                                                                                                                          f
                                                                                                                        |);
                                                                                                                        M.read (|
                                                                                                                          c
                                                                                                                        |)
                                                                                                                      ]
                                                                                                                    |)
                                                                                                                  ]
                                                                                                                |)
                                                                                                              |),
                                                                                                              [
                                                                                                                fun
                                                                                                                    γ =>
                                                                                                                  ltac:(M.monadic
                                                                                                                    (let
                                                                                                                          γ0_0 :=
                                                                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                                                                        γ,
                                                                                                                        "core::ops::control_flow::ControlFlow::Break",
                                                                                                                        0
                                                                                                                      |) in
                                                                                                                    let
                                                                                                                          residual :=
                                                                                                                      M.copy (|
                                                                                                                        γ0_0
                                                                                                                      |) in
                                                                                                                    M.alloc (|
                                                                                                                      M.never_to_any (|
                                                                                                                        M.read (|
                                                                                                                          M.return_ (|
                                                                                                                            M.call_closure (|
                                                                                                                              M.get_trait_method (|
                                                                                                                                "core::ops::try_trait::FromResidual",
                                                                                                                                Ty.apply
                                                                                                                                  (Ty.path
                                                                                                                                    "core::result::Result")
                                                                                                                                  []
                                                                                                                                  [
                                                                                                                                    Ty.tuple
                                                                                                                                      [];
                                                                                                                                    Ty.path
                                                                                                                                      "core::fmt::Error"
                                                                                                                                  ],
                                                                                                                                [
                                                                                                                                  Ty.apply
                                                                                                                                    (Ty.path
                                                                                                                                      "core::result::Result")
                                                                                                                                    []
                                                                                                                                    [
                                                                                                                                      Ty.path
                                                                                                                                        "core::convert::Infallible";
                                                                                                                                      Ty.path
                                                                                                                                        "core::fmt::Error"
                                                                                                                                    ]
                                                                                                                                ],
                                                                                                                                "from_residual",
                                                                                                                                []
                                                                                                                              |),
                                                                                                                              [
                                                                                                                                M.read (|
                                                                                                                                  residual
                                                                                                                                |)
                                                                                                                              ]
                                                                                                                            |)
                                                                                                                          |)
                                                                                                                        |)
                                                                                                                      |)
                                                                                                                    |)));
                                                                                                                fun
                                                                                                                    γ =>
                                                                                                                  ltac:(M.monadic
                                                                                                                    (let
                                                                                                                          γ0_0 :=
                                                                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                                                                        γ,
                                                                                                                        "core::ops::control_flow::ControlFlow::Continue",
                                                                                                                        0
                                                                                                                      |) in
                                                                                                                    let
                                                                                                                          val :=
                                                                                                                      M.copy (|
                                                                                                                        γ0_0
                                                                                                                      |) in
                                                                                                                    val))
                                                                                                              ]
                                                                                                            |) in
                                                                                                          M.alloc (|
                                                                                                            Value.Tuple
                                                                                                              []
                                                                                                          |)))
                                                                                                    ]
                                                                                                  |) in
                                                                                                M.alloc (|
                                                                                                  Value.Tuple
                                                                                                    []
                                                                                                |)))
                                                                                            |)))
                                                                                      ]
                                                                                    |)) in
                                                                                let~ _ :=
                                                                                  M.write (|
                                                                                    from,
                                                                                    BinOp.Wrap.add (|
                                                                                      M.read (|
                                                                                        i
                                                                                      |),
                                                                                      M.call_closure (|
                                                                                        M.get_associated_function (|
                                                                                          Ty.path
                                                                                            "char",
                                                                                          "len_utf8",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.read (|
                                                                                            c
                                                                                          |)
                                                                                        ]
                                                                                      |)
                                                                                    |)
                                                                                  |) in
                                                                                M.alloc (|
                                                                                  Value.Tuple []
                                                                                |)));
                                                                            fun γ =>
                                                                              ltac:(M.monadic
                                                                                (M.alloc (|
                                                                                  Value.Tuple []
                                                                                |)))
                                                                          ]
                                                                        |)))
                                                                  ]
                                                                |) in
                                                              M.alloc (| Value.Tuple [] |)))
                                                          |)))
                                                    ]
                                                  |)) in
                                              let~ _ :=
                                                M.match_operator (|
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::try_trait::Try",
                                                        Ty.apply
                                                          (Ty.path "core::result::Result")
                                                          []
                                                          [ Ty.tuple []; Ty.path "core::fmt::Error"
                                                          ],
                                                        [],
                                                        "branch",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::Formatter",
                                                            "write_str",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| f |);
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::index::Index",
                                                                Ty.path "str",
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "core::ops::range::RangeFrom")
                                                                    []
                                                                    [ Ty.path "usize" ]
                                                                ],
                                                                "index",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| valid |);
                                                                Value.StructRecord
                                                                  "core::ops::range::RangeFrom"
                                                                  [ ("start", M.read (| from |)) ]
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "core::ops::control_flow::ControlFlow::Break",
                                                            0
                                                          |) in
                                                        let residual := M.copy (| γ0_0 |) in
                                                        M.alloc (|
                                                          M.never_to_any (|
                                                            M.read (|
                                                              M.return_ (|
                                                                M.call_closure (|
                                                                  M.get_trait_method (|
                                                                    "core::ops::try_trait::FromResidual",
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::result::Result")
                                                                      []
                                                                      [
                                                                        Ty.tuple [];
                                                                        Ty.path "core::fmt::Error"
                                                                      ],
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::result::Result")
                                                                        []
                                                                        [
                                                                          Ty.path
                                                                            "core::convert::Infallible";
                                                                          Ty.path "core::fmt::Error"
                                                                        ]
                                                                    ],
                                                                    "from_residual",
                                                                    []
                                                                  |),
                                                                  [ M.read (| residual |) ]
                                                                |)
                                                              |)
                                                            |)
                                                          |)
                                                        |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "core::ops::control_flow::ControlFlow::Continue",
                                                            0
                                                          |) in
                                                        let val := M.copy (| γ0_0 |) in
                                                        val))
                                                  ]
                                                |) in
                                              M.alloc (| Value.Tuple [] |) in
                                            M.use
                                              (M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::iter::traits::collect::IntoIterator",
                                                      Ty.apply
                                                        (Ty.path "&")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path "slice")
                                                            []
                                                            [ Ty.path "u8" ]
                                                        ],
                                                      [],
                                                      "into_iter",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::str::lossy::Utf8Chunk",
                                                          "invalid",
                                                          []
                                                        |),
                                                        [ chunk ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let iter := M.copy (| γ |) in
                                                      M.loop (|
                                                        ltac:(M.monadic
                                                          (let~ _ :=
                                                            M.match_operator (|
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_trait_method (|
                                                                    "core::iter::traits::iterator::Iterator",
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::slice::iter::Iter")
                                                                      []
                                                                      [ Ty.path "u8" ],
                                                                    [],
                                                                    "next",
                                                                    []
                                                                  |),
                                                                  [ iter ]
                                                                |)
                                                              |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let _ :=
                                                                      M.is_struct_tuple (|
                                                                        γ,
                                                                        "core::option::Option::None"
                                                                      |) in
                                                                    M.alloc (|
                                                                      M.never_to_any (|
                                                                        M.read (| M.break (||) |)
                                                                      |)
                                                                    |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ0_0 :=
                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                        γ,
                                                                        "core::option::Option::Some",
                                                                        0
                                                                      |) in
                                                                    let γ0_0 := M.read (| γ0_0 |) in
                                                                    let b := M.copy (| γ0_0 |) in
                                                                    let~ _ :=
                                                                      M.match_operator (|
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_trait_method (|
                                                                              "core::ops::try_trait::Try",
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "core::result::Result")
                                                                                []
                                                                                [
                                                                                  Ty.tuple [];
                                                                                  Ty.path
                                                                                    "core::fmt::Error"
                                                                                ],
                                                                              [],
                                                                              "branch",
                                                                              []
                                                                            |),
                                                                            [
                                                                              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_formatted",
                                                                                      []
                                                                                    |),
                                                                                    [
                                                                                      M.alloc (|
                                                                                        Value.Array
                                                                                          [
                                                                                            M.read (|
                                                                                              Value.String
                                                                                                "\x"
                                                                                            |)
                                                                                          ]
                                                                                      |);
                                                                                      M.alloc (|
                                                                                        Value.Array
                                                                                          [
                                                                                            M.call_closure (|
                                                                                              M.get_associated_function (|
                                                                                                Ty.path
                                                                                                  "core::fmt::rt::Argument",
                                                                                                "new_upper_hex",
                                                                                                [
                                                                                                  Ty.path
                                                                                                    "u8"
                                                                                                ]
                                                                                              |),
                                                                                              [ b ]
                                                                                            |)
                                                                                          ]
                                                                                      |);
                                                                                      M.alloc (|
                                                                                        Value.Array
                                                                                          [
                                                                                            M.call_closure (|
                                                                                              M.get_associated_function (|
                                                                                                Ty.path
                                                                                                  "core::fmt::rt::Placeholder",
                                                                                                "new",
                                                                                                []
                                                                                              |),
                                                                                              [
                                                                                                Value.Integer
                                                                                                  IntegerKind.Usize
                                                                                                  0;
                                                                                                Value.UnicodeChar
                                                                                                  32;
                                                                                                Value.StructTuple
                                                                                                  "core::fmt::rt::Alignment::Unknown"
                                                                                                  [];
                                                                                                Value.Integer
                                                                                                  IntegerKind.U32
                                                                                                  8;
                                                                                                Value.StructTuple
                                                                                                  "core::fmt::rt::Count::Implied"
                                                                                                  [];
                                                                                                Value.StructTuple
                                                                                                  "core::fmt::rt::Count::Is"
                                                                                                  [
                                                                                                    Value.Integer
                                                                                                      IntegerKind.Usize
                                                                                                      2
                                                                                                  ]
                                                                                              ]
                                                                                            |)
                                                                                          ]
                                                                                      |);
                                                                                      M.call_closure (|
                                                                                        M.get_associated_function (|
                                                                                          Ty.path
                                                                                            "core::fmt::rt::UnsafeArg",
                                                                                          "new",
                                                                                          []
                                                                                        |),
                                                                                        []
                                                                                      |)
                                                                                    ]
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            ]
                                                                          |)
                                                                        |),
                                                                        [
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let γ0_0 :=
                                                                                M.SubPointer.get_struct_tuple_field (|
                                                                                  γ,
                                                                                  "core::ops::control_flow::ControlFlow::Break",
                                                                                  0
                                                                                |) in
                                                                              let residual :=
                                                                                M.copy (| γ0_0 |) in
                                                                              M.alloc (|
                                                                                M.never_to_any (|
                                                                                  M.read (|
                                                                                    M.return_ (|
                                                                                      M.call_closure (|
                                                                                        M.get_trait_method (|
                                                                                          "core::ops::try_trait::FromResidual",
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "core::result::Result")
                                                                                            []
                                                                                            [
                                                                                              Ty.tuple
                                                                                                [];
                                                                                              Ty.path
                                                                                                "core::fmt::Error"
                                                                                            ],
                                                                                          [
                                                                                            Ty.apply
                                                                                              (Ty.path
                                                                                                "core::result::Result")
                                                                                              []
                                                                                              [
                                                                                                Ty.path
                                                                                                  "core::convert::Infallible";
                                                                                                Ty.path
                                                                                                  "core::fmt::Error"
                                                                                              ]
                                                                                          ],
                                                                                          "from_residual",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.read (|
                                                                                            residual
                                                                                          |)
                                                                                        ]
                                                                                      |)
                                                                                    |)
                                                                                  |)
                                                                                |)
                                                                              |)));
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let γ0_0 :=
                                                                                M.SubPointer.get_struct_tuple_field (|
                                                                                  γ,
                                                                                  "core::ops::control_flow::ControlFlow::Continue",
                                                                                  0
                                                                                |) in
                                                                              let val :=
                                                                                M.copy (| γ0_0 |) in
                                                                              val))
                                                                        ]
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)))
                                                              ]
                                                            |) in
                                                          M.alloc (| Value.Tuple [] |)))
                                                      |)))
                                                ]
                                              |))))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                              |)))
                        ]
                      |)) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::fmt::Write",
                        Ty.path "core::fmt::Formatter",
                        [],
                        "write_char",
                        []
                      |),
                      [ M.read (| f |); Value.UnicodeChar 34 ]
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => 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_lossy_Debug.
    
    (* StructRecord
      {
        name := "Utf8Chunks";
        const_params := [];
        ty_params := [];
        fields :=
          [ ("source", Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ])
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_core_str_lossy_Utf8Chunks.
      Definition Self : Ty.t := Ty.path "core::str::lossy::Utf8Chunks".
      
      (* 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::str::lossy::Utf8Chunks"
              [
                ("source",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::str::lossy::Utf8Chunks",
                        "source"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_lossy_Utf8Chunks.
    
    Module Impl_core_str_lossy_Utf8Chunks.
      Definition Self : Ty.t := Ty.path "core::str::lossy::Utf8Chunks".
      
      (*
          pub fn debug(&self) -> Debug<'_> {
              Debug(self.source)
          }
      *)
      Definition debug (ε : 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::lossy::Debug"
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::str::lossy::Utf8Chunks",
                    "source"
                  |)
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_debug : M.IsAssociatedFunction Self "debug" debug.
    End Impl_core_str_lossy_Utf8Chunks.
    
    Module Impl_core_iter_traits_iterator_Iterator_for_core_str_lossy_Utf8Chunks.
      Definition Self : Ty.t := Ty.path "core::str::lossy::Utf8Chunks".
      
      (*     type Item = Utf8Chunk<'a>; *)
      Definition _Item : Ty.t := Ty.path "core::str::lossy::Utf8Chunk".
      
      (*
          fn next(&mut self) -> Option<Utf8Chunk<'a>> {
              if self.source.is_empty() {
                  return None;
              }
      
              const TAG_CONT_U8: u8 = 128;
              fn safe_get(xs: &[u8], i: usize) -> u8 {
                  *xs.get(i).unwrap_or(&0)
              }
      
              let mut i = 0;
              let mut valid_up_to = 0;
              while i < self.source.len() {
                  // SAFETY: `i < self.source.len()` per previous line.
                  // For some reason the following are both significantly slower:
                  // while let Some(&byte) = self.source.get(i) {
                  // while let Some(byte) = self.source.get(i).copied() {
                  let byte = unsafe { *self.source.get_unchecked(i) };
                  i += 1;
      
                  if byte < 128 {
                      // This could be a `1 => ...` case in the match below, but for
                      // the common case of all-ASCII inputs, we bypass loading the
                      // sizeable UTF8_CHAR_WIDTH table into cache.
                  } else {
                      let w = utf8_char_width(byte);
      
                      match w {
                          2 => {
                              if safe_get(self.source, i) & 192 != TAG_CONT_U8 {
                                  break;
                              }
                              i += 1;
                          }
                          3 => {
                              match (byte, safe_get(self.source, i)) {
                                  (0xE0, 0xA0..=0xBF) => (),
                                  (0xE1..=0xEC, 0x80..=0xBF) => (),
                                  (0xED, 0x80..=0x9F) => (),
                                  (0xEE..=0xEF, 0x80..=0xBF) => (),
                                  _ => break,
                              }
                              i += 1;
                              if safe_get(self.source, i) & 192 != TAG_CONT_U8 {
                                  break;
                              }
                              i += 1;
                          }
                          4 => {
                              match (byte, safe_get(self.source, i)) {
                                  (0xF0, 0x90..=0xBF) => (),
                                  (0xF1..=0xF3, 0x80..=0xBF) => (),
                                  (0xF4, 0x80..=0x8F) => (),
                                  _ => break,
                              }
                              i += 1;
                              if safe_get(self.source, i) & 192 != TAG_CONT_U8 {
                                  break;
                              }
                              i += 1;
                              if safe_get(self.source, i) & 192 != TAG_CONT_U8 {
                                  break;
                              }
                              i += 1;
                          }
                          _ => break,
                      }
                  }
      
                  valid_up_to = i;
              }
      
              // SAFETY: `i <= self.source.len()` because it is only ever incremented
              // via `i += 1` and in between every single one of those increments, `i`
              // is compared against `self.source.len()`. That happens either
              // literally by `i < self.source.len()` in the while-loop's condition,
              // or indirectly by `safe_get(self.source, i) & 192 != TAG_CONT_U8`. The
              // loop is terminated as soon as the latest `i += 1` has made `i` no
              // longer less than `self.source.len()`, which means it'll be at most
              // equal to `self.source.len()`.
              let (inspected, remaining) = unsafe { self.source.split_at_unchecked(i) };
              self.source = remaining;
      
              // SAFETY: `valid_up_to <= i` because it is only ever assigned via
              // `valid_up_to = i` and `i` only increases.
              let (valid, invalid) = unsafe { inspected.split_at_unchecked(valid_up_to) };
      
              Some(Utf8Chunk {
                  // SAFETY: All bytes up to `valid_up_to` are valid UTF-8.
                  valid: unsafe { from_utf8_unchecked(valid) },
                  invalid,
              })
          }
      *)
      Definition next (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    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 "slice") [] [ Ty.path "u8" ],
                                      "is_empty",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "core::str::lossy::Utf8Chunks",
                                          "source"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (| Value.StructTuple "core::option::Option::None" [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ i := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                  let~ valid_up_to := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                  let~ _ :=
                    M.loop (|
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.lt (|
                                        M.read (| i |),
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                            "len",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "core::str::lossy::Utf8Chunks",
                                                "source"
                                              |)
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ byte :=
                                  M.copy (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                        "get_unchecked",
                                        [ Ty.path "usize" ]
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::str::lossy::Utf8Chunks",
                                            "source"
                                          |)
                                        |);
                                        M.read (| i |)
                                      ]
                                    |)
                                  |) in
                                let~ _ :=
                                  let β := i in
                                  M.write (|
                                    β,
                                    BinOp.Wrap.add (|
                                      M.read (| β |),
                                      Value.Integer IntegerKind.Usize 1
                                    |)
                                  |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.lt (|
                                                  M.read (| byte |),
                                                  Value.Integer IntegerKind.U8 128
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (| Value.Tuple [] |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let~ w :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_function (|
                                                  "core::str::validations::utf8_char_width",
                                                  []
                                                |),
                                                [ M.read (| byte |) ]
                                              |)
                                            |) in
                                          M.match_operator (|
                                            w,
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Integer IntegerKind.Usize 2
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  BinOp.ne (|
                                                                    BinOp.bit_and
                                                                      (M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Self,
                                                                          "safe_get.next",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "core::str::lossy::Utf8Chunks",
                                                                              "source"
                                                                            |)
                                                                          |);
                                                                          M.read (| i |)
                                                                        ]
                                                                      |))
                                                                      (Value.Integer
                                                                        IntegerKind.U8
                                                                        192),
                                                                    M.read (|
                                                                      M.get_constant (|
                                                                        "core::str::lossy::next::TAG_CONT_U8"
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (| M.break (||) |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  let~ _ :=
                                                    let β := i in
                                                    M.write (|
                                                      β,
                                                      BinOp.Wrap.add (|
                                                        M.read (| β |),
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Integer IntegerKind.Usize 3
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        Value.Tuple
                                                          [
                                                            M.read (| byte |);
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Self,
                                                                "safe_get.next",
                                                                []
                                                              |),
                                                              [
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| self |),
                                                                    "core::str::lossy::Utf8Chunks",
                                                                    "source"
                                                                  |)
                                                                |);
                                                                M.read (| i |)
                                                              ]
                                                            |)
                                                          ]
                                                      |),
                                                      [
                                                        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 _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ0_0 |),
                                                                Value.Integer IntegerKind.U8 224
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_tuple_field (|
                                                                γ,
                                                                0
                                                              |) in
                                                            let γ0_1 :=
                                                              M.SubPointer.get_tuple_field (|
                                                                γ,
                                                                1
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)));
                                                        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 _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ0_0 |),
                                                                Value.Integer IntegerKind.U8 237
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_tuple_field (|
                                                                γ,
                                                                0
                                                              |) in
                                                            let γ0_1 :=
                                                              M.SubPointer.get_tuple_field (|
                                                                γ,
                                                                1
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (| M.break (||) |)
                                                              |)
                                                            |)))
                                                      ]
                                                    |) in
                                                  let~ _ :=
                                                    let β := i in
                                                    M.write (|
                                                      β,
                                                      BinOp.Wrap.add (|
                                                        M.read (| β |),
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  BinOp.ne (|
                                                                    BinOp.bit_and
                                                                      (M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Self,
                                                                          "safe_get.next",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "core::str::lossy::Utf8Chunks",
                                                                              "source"
                                                                            |)
                                                                          |);
                                                                          M.read (| i |)
                                                                        ]
                                                                      |))
                                                                      (Value.Integer
                                                                        IntegerKind.U8
                                                                        192),
                                                                    M.read (|
                                                                      M.get_constant (|
                                                                        "core::str::lossy::next::TAG_CONT_U8"
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (| M.break (||) |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  let~ _ :=
                                                    let β := i in
                                                    M.write (|
                                                      β,
                                                      BinOp.Wrap.add (|
                                                        M.read (| β |),
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Integer IntegerKind.Usize 4
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        Value.Tuple
                                                          [
                                                            M.read (| byte |);
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Self,
                                                                "safe_get.next",
                                                                []
                                                              |),
                                                              [
                                                                M.read (|
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| self |),
                                                                    "core::str::lossy::Utf8Chunks",
                                                                    "source"
                                                                  |)
                                                                |);
                                                                M.read (| i |)
                                                              ]
                                                            |)
                                                          ]
                                                      |),
                                                      [
                                                        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 _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ0_0 |),
                                                                Value.Integer IntegerKind.U8 240
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_tuple_field (|
                                                                γ,
                                                                0
                                                              |) in
                                                            let γ0_1 :=
                                                              M.SubPointer.get_tuple_field (|
                                                                γ,
                                                                1
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)));
                                                        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 _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ0_0 |),
                                                                Value.Integer IntegerKind.U8 244
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (| M.break (||) |)
                                                              |)
                                                            |)))
                                                      ]
                                                    |) in
                                                  let~ _ :=
                                                    let β := i in
                                                    M.write (|
                                                      β,
                                                      BinOp.Wrap.add (|
                                                        M.read (| β |),
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  BinOp.ne (|
                                                                    BinOp.bit_and
                                                                      (M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Self,
                                                                          "safe_get.next",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "core::str::lossy::Utf8Chunks",
                                                                              "source"
                                                                            |)
                                                                          |);
                                                                          M.read (| i |)
                                                                        ]
                                                                      |))
                                                                      (Value.Integer
                                                                        IntegerKind.U8
                                                                        192),
                                                                    M.read (|
                                                                      M.get_constant (|
                                                                        "core::str::lossy::next::TAG_CONT_U8"
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (| M.break (||) |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  let~ _ :=
                                                    let β := i in
                                                    M.write (|
                                                      β,
                                                      BinOp.Wrap.add (|
                                                        M.read (| β |),
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  BinOp.ne (|
                                                                    BinOp.bit_and
                                                                      (M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Self,
                                                                          "safe_get.next",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "core::str::lossy::Utf8Chunks",
                                                                              "source"
                                                                            |)
                                                                          |);
                                                                          M.read (| i |)
                                                                        ]
                                                                      |))
                                                                      (Value.Integer
                                                                        IntegerKind.U8
                                                                        192),
                                                                    M.read (|
                                                                      M.get_constant (|
                                                                        "core::str::lossy::next::TAG_CONT_U8"
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (| M.break (||) |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  let~ _ :=
                                                    let β := i in
                                                    M.write (|
                                                      β,
                                                      BinOp.Wrap.add (|
                                                        M.read (| β |),
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.alloc (|
                                                    M.never_to_any (| M.read (| M.break (||) |) |)
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                let~ _ := M.write (| valid_up_to, M.read (| i |) |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      let~ _ :=
                                        M.alloc (|
                                          M.never_to_any (| M.read (| M.break (||) |) |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)))
                    |) in
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "split_at_unchecked",
                          []
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::str::lossy::Utf8Chunks",
                              "source"
                            |)
                          |);
                          M.read (| i |)
                        ]
                      |)
                    |),
                    [
                      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 inspected := M.copy (| γ0_0 |) in
                          let remaining := M.copy (| γ0_1 |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::str::lossy::Utf8Chunks",
                                "source"
                              |),
                              M.read (| remaining |)
                            |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                  "split_at_unchecked",
                                  []
                                |),
                                [ M.read (| inspected |); M.read (| valid_up_to |) ]
                              |)
                            |),
                            [
                              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 valid := M.copy (| γ0_0 |) in
                                  let invalid := M.copy (| γ0_1 |) in
                                  M.alloc (|
                                    Value.StructTuple
                                      "core::option::Option::Some"
                                      [
                                        Value.StructRecord
                                          "core::str::lossy::Utf8Chunk"
                                          [
                                            ("valid",
                                              M.call_closure (|
                                                M.get_function (|
                                                  "core::str::converts::from_utf8_unchecked",
                                                  []
                                                |),
                                                [ M.read (| valid |) ]
                                              |));
                                            ("invalid", M.read (| invalid |))
                                          ]
                                      ]
                                  |)))
                            ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("Item", InstanceField.Ty _Item); ("next", InstanceField.Method next) ].
    End Impl_core_iter_traits_iterator_Iterator_for_core_str_lossy_Utf8Chunks.
    
    Module Impl_core_iter_traits_marker_FusedIterator_for_core_str_lossy_Utf8Chunks.
      Definition Self : Ty.t := Ty.path "core::str::lossy::Utf8Chunks".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_for_core_str_lossy_Utf8Chunks.
    
    Module Impl_core_fmt_Debug_for_core_str_lossy_Utf8Chunks.
      Definition Self : Ty.t := Ty.path "core::str::lossy::Utf8Chunks".
      
      (*
          fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
              f.debug_struct("Utf8Chunks").field("source", &self.debug()).finish()
          }
      *)
      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::builders::DebugStruct",
                "finish",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugStruct",
                    "field",
                    []
                  |),
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_struct",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Utf8Chunks" |) ]
                      |)
                    |);
                    M.read (| Value.String "source" |);
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::str::lossy::Utf8Chunks",
                          "debug",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => 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_lossy_Utf8Chunks.
  End lossy.
End str.
