727def telemetryRecordWordRequired =
728 (lambda unrestricted parts : (family TelemetryRecordParts) .
729 (lambda unrestricted index : Nat .
730 (let unrestricted start =
731 (telemetryCapturedWordAt index)
732 in
733 (let unrestricted end =
734 (naturalAdd start captureWordBytes)
735 in
736 (eliminate
737 TelemetryRecordParts
738 (lambda unrestricted current : (family TelemetryRecordParts) . Nat)
739 parts
740 (branch TelemetryRecordEnd . 0)
741 (branch TelemetryRecordLiteral bytes tail induction . induction)
742 (branch
743 TelemetryRecordDecimal
744 signed
745 offset
746 tail
747 induction
748 .
749 (naturalOr
750 induction
751 (naturalAnd
752 (naturalLess index captureValueWords)
753 (naturalAnd
754 (naturalLess start (naturalAdd offset captureWordBytes))
755 (naturalLess offset end)))))
756 (branch
757 TelemetryRecordHex
758 source
759 offset
760 width
761 reverse
762 nonzero
763 tail
764 induction
765 .
766 (naturalOr
767 induction
768 (naturalAnd
769 (naturalEqual source 0)
770 (naturalAnd
771 (naturalLess index captureValueWords)
772 (naturalAnd
773 (naturalLess start (naturalAdd offset width))
774 (naturalLess offset end)))))))))))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.