848def quotedDecodeTextLiteral =
849 (lambda unrestricted spelling : Bytes .
850 (eliminate
851 UTF8DecodeResult
852 (lambda unrestricted decoded : (family UTF8DecodeResult) . (family QuotedLiteralResult))
853 (Data.UTF8/decodeUTF8 spelling)
854 (branch
855 UTF8DecodeSucceeded
856 points
857 .
858 (quotedChoose
859 (byte-equal (bytes-head spelling) (byte 34))
860 (lambda unrestricted force : Nat . (quotedDecodeTextBody (bytes-tail spelling)))
861 (lambda unrestricted force : Nat .
862 (constructor
863 QuotedLiteralResult
864 QuotedLiteralFailed
865 (constructor QuotedLiteralFailure QuotedInvalidPrefix)
866 zero
867 zero))))
868 (branch
869 UTF8DecodeFailed
870 failure
871 offset
872 .
873 (constructor
874 QuotedLiteralResult
875 QuotedLiteralFailed
876 (constructor QuotedLiteralFailure QuotedInvalidUTF8)
877 (Model.Word32/modelWord32ToNatural offset)
878 (succ (Model.Word32/modelWord32ToNatural offset))))))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.