---------------------------------------------------------------------------
Lines
a line: parsed within the stream limits, then checked
618def aosClassifyLine =
619 (lambda unrestricted line : Bytes .
620 (eliminate
621 JSONDocumentResult
622 (lambda unrestricted current : (family JSONDocumentResult) . (family AosLine))
623 (parseJSONWithLimits aosLimits line)
624 (branch
625 JSONDocumentParsed
626 record
627 .
628 (let unrestricted code =
629 (aosRecordCode record)
630 in
631 (nat-eliminate
632 (lambda unrestricted current : Nat . (family AosLine))
633 (constructor AosLine AosLineValid record)
634 (lambda unrestricted predecessor : Nat .
635 (lambda unrestricted induction : (family AosLine) .
636 (constructor AosLine AosLineInvalid code)))
637 code)))
638 (branch
639 JSONDocumentFailed
640 error
641 offset
642 .
643 (constructor AosLine AosLineInvalid (aosParseErrorCode error)))))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.