439def quotedDecodeByteLiteral =
440 (lambda unrestricted spelling : Bytes .
441 (quotedChoose
442 (byte-equal (bytes-head spelling) (byte 98))
443 (lambda unrestricted force : Nat .
444 (quotedChoose
445 (byte-equal (bytes-head (bytes-tail spelling)) (byte 34))
446 (lambda unrestricted force : Nat .
447 (decodeByteLiteralBody (bytes-tail (bytes-tail spelling))))
448 (lambda unrestricted force : Nat .
449 (constructor
450 QuotedLiteralResult
451 QuotedLiteralFailed
452 (constructor QuotedLiteralFailure QuotedInvalidPrefix)
453 zero
454 zero))))
455 (lambda unrestricted force : Nat .
456 (constructor
457 QuotedLiteralResult
458 QuotedLiteralFailed
459 (constructor QuotedLiteralFailure QuotedInvalidPrefix)
460 zero
461 zero))))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.