484def publicationTypedLineAdmission =
485 (lambda unrestricted binding : Bytes .
486 (lambda unrestricted lower : Nat .
487 (lambda unrestricted upper : Nat .
488 (lambda unrestricted line : Bytes .
489 (naturalAnd
490 (naturalIsZero
491 (aosAnyByte (lambda unrestricted b : Byte . (byte-equal b (byte 10))) line))
492 (eliminate
493 AosLine
494 (lambda unrestricted current : (family AosLine) . Nat)
495 (aosClassifyLine line)
496 (branch AosLineInvalid code . 0)
497 (branch
498 AosLineValid
499 record
500 .
501 (aosChoose
502 Nat
503 (bytes-equal (aosMemberBytes b"type" record) b"descriptor")
504 (naturalIsZero (bytes-equal (aosMemberBytes b"kind" record) b"attempt"))
505 (naturalAnd
506 (bytes-equal (aosMemberBytes b"type" record) b"event")
507 (let unrestricted identity =
508 (aosMemberValue b"event_id" record)
509 in
510 (naturalAnd
511 (bytes-equal binding (aosProducerKeyOf identity))
512 (publicationSequenceAdmission
513 lower
514 upper
515 (aosDigitsValue (aosMemberBytes b"sequence" identity))))))))))))))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.