the complete lines (every segment but the last), walked in order from
line 1: a left fold, the walk threaded through the right fold's functions
686def aosWalkLinesFrom =
687 (lambda unrestricted initial : (family AosWalk) .
688 (lambda unrestricted firstLine : Nat .
689 (lambda unrestricted segments : (family StdList Bytes) .
690 (app
691 (eliminate
692 StdList
693 (lambda unrestricted current : (family StdList Bytes) .
694 (pi unrestricted walk : (family AosWalk) .
695 (pi unrestricted n : Nat . (family AosWalk))))
696 segments
697 (branch
698 StdListEmpty
699 .
700 (lambda unrestricted walk : (family AosWalk) . (lambda unrestricted n : Nat . walk)))
701 (branch
702 StdListCons
703 line
704 rest
705 induction
706 .
707 (lambda unrestricted walk : (family AosWalk) .
708 (lambda unrestricted n : Nat .
709 -- the last segment is not a line: it is the tail after the last LF
710 (aosChoose
711 (family AosWalk)
712 (naturalIsZero (aosListLength rest))
713 walk
714 (induction (aosWalkLine walk n line) (succ n)))))))
715 initial
716 firstLine))))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.