@[simp]

theorem String.fromUTF8Lossy_empty : fromUTF8Lossy ByteArray.empty = ""

theorem String.fromUTF8Lossy_of_utf8DecodeChar?_eq_some {b : ByteArray} {c : Char} (hc : b.utf8DecodeChar? 0 = some c) : fromUTF8Lossy b = singleton c ++ fromUTF8Lossy (b.extract c.utf8Size b.size)

theorem String.fromUTF8Lossy_utf8Encode_singleton_append {b : ByteArray} {c : Char} : fromUTF8Lossy ([c].utf8Encode ++ b) = singleton c ++ fromUTF8Lossy b

theorem String.fromUTF8Lossy_utf8Encode_append {l : List Char} {b : ByteArray} : fromUTF8Lossy (l.utf8Encode ++ b) = ofList l ++ fromUTF8Lossy b

@[simp]

theorem String.fromUTF8Lossy_utf8Encode {l : List Char} : fromUTF8Lossy l.utf8Encode = ofList l

theorem String.fromUTF8Lossy_eq_of_isValidUTF8 {b : ByteArray} (h : b.IsValidUTF8) : fromUTF8Lossy b = { toByteArray := b, isValidUTF8 := h }

@[simp]

theorem String.fromUTF8Lossy_toByteArray {s : String} : fromUTF8Lossy s.toByteArray = s

theorem String.fromUTF8Lossy_append_of_utf8DecodeChar?_eq_none {l b : ByteArray} (hl : 0 < l.size) (h : (l ++ b).utf8DecodeChar? 0 = none) (hcont : ∀ (i : Nat) (hi : i < l.size), 0 < i → l[i].isUTF8ContinuationByte = true) (hb : ∀ (h : 0 < b.size), ¬b[0].isUTF8ContinuationByte = true) : fromUTF8Lossy (l ++ b) = singleton '�' ++ fromUTF8Lossy b

If decoding l ++ b fails at the first byte, all other bytes of l are continuation bytes and b does not start with a continuation byte, then fromUTF8Lossy replaces l with a single � and continues with b.

theorem String.fromUTF8Lossy_surrogate_append {x y : UInt8} {b : ByteArray} (hx : 160 ≤ x ∧ x < 192) (hy : 128 ≤ y ∧ y < 192) (hb : ∀ (h : 0 < b.size), ¬b[0].isUTF8ContinuationByte = true) : fromUTF8Lossy ([237, x, y].toByteArray ++ b) = singleton '�' ++ fromUTF8Lossy b

The bytes 0xED x y with 0xA0 ≤ x < 0xC0 and 0x80 ≤ y < 0xC0 would encode a surrogate code point (U+D800 to U+DFFF), so fromUTF8Lossy replaces them with a single �, provided that b does not start with a continuation byte.