Text and the compiler share this validity decision with the existing decoder.
No replacement character, normalization or second validation machine.
1291def stdUtf8Valid : (pi unrestricted input : Bytes . (family StdBool)) =
1292 (lambda unrestricted input : Bytes .
1293 (eliminate
1294 UTF8DecodeResult
1295 (lambda unrestricted result : (family UTF8DecodeResult) . (family StdBool))
1296 (decodeUTF8 input)
1297 (branch UTF8DecodeSucceeded codepoints . (constructor StdBool StdTrue))
1298 (branch UTF8DecodeFailed error offset . (constructor StdBool StdFalse))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.