the footer: it counts the lines before it
548def aosWalkFooter =
549 (lambda unrestricted walk : (family AosWalk) .
550 (lambda unrestricted n : Nat .
551 (lambda unrestricted record : (family JSON) .
552 (eliminate
553 AosWalk
554 (lambda unrestricted current : (family AosWalk) . (family AosWalk))
555 walk
556 (branch
557 AosWalkValue
558 problem
559 line
560 code
561 producers
562 footer
563 complete
564 events
565 unknown
566 .
567 (aosChoose
568 (family AosWalk)
569 (naturalEqual (aosDecimalOf b"records" record) (naturalSaturatingSubtract n 1))
570 (constructor
571 AosWalk
572 AosWalkValue
573 problem
574 line
575 code
576 producers
577 1
578 (aosBooleanFlag (aosMemberValue b"complete" record))
579 events
580 unknown)
581 (aosWalkFail walk 5 n 0)))))))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.