a valid record at line n
629def aosWalkRecord =
630 (lambda unrestricted walk : (family AosWalk) .
631 (lambda unrestricted n : Nat .
632 (lambda unrestricted record : (family JSON) .
633 (let unrestricted kind =
634 (aosMemberBytes b"type" record)
635 in
636 (aosChoose
637 (family AosWalk)
638 (naturalEqual n 1)
639 (aosChoose (family AosWalk) (bytes-equal kind b"header") walk (aosWalkFail walk 3 1 0))
640 (aosChoose
641 (family AosWalk)
642 (bytes-equal kind b"event")
643 (aosWalkEvent walk n record)
644 (aosChoose
645 (family AosWalk)
646 (bytes-equal kind b"coverage")
647 (aosWalkCoverage walk n record)
648 (aosChoose
649 (family AosWalk)
650 (bytes-equal kind b"footer")
651 (aosWalkFooter walk n record)
652 (aosChoose
653 (family AosWalk)
654 (naturalOr
655 (bytes-equal kind b"header")
656 (naturalOr (bytes-equal kind b"descriptor") (bytes-equal kind b"artifact")))
657 walk
658 (aosWalkUnknownRecord walk))))))))))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.