741def parserStripByteStep =
742 (lambda unrestricted head : Byte .
743 (lambda unrestricted state : Nat .
744 (nat-eliminate
745 (lambda unrestricted stateZero : Nat . (family ParserStripStep))
746 (parserStripBetweenStep head)
747 (lambda unrestricted stateOne : Nat .
748 (lambda unrestricted inductionOne : (family ParserStripStep) .
749 (nat-eliminate
750 (lambda unrestricted innerOne : Nat . (family ParserStripStep))
751 (parserStripTokenStep head)
752 (lambda unrestricted stateTwo : Nat .
753 (lambda unrestricted inductionTwo : (family ParserStripStep) .
754 (nat-eliminate
755 (lambda unrestricted innerTwo : Nat . (family ParserStripStep))
756 (parserStripPendingStep head)
757 (lambda unrestricted stateThree : Nat .
758 (lambda unrestricted inductionThree : (family ParserStripStep) .
759 (parserStripCommentStep head)))
760 stateTwo)))
761 stateOne)))
762 state)))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.