695def dataBytesBuilderChunkWithin =
696 (lambda unrestricted allocationLimit : Nat .
697 (lambda unrestricted chunk : Bytes .
698 (app
699 (lambda unrestricted chunkLength : Nat .
700 (nat-eliminate
701 (lambda unrestricted current : Nat . (family DataBytesBuilderResult))
702 (constructor
703 DataBytesBuilderResult
704 DataBytesBuilderFailed
705 (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded)
706 (dataBytesTelemetry chunkLength chunkLength zero zero zero zero zero allocationLimit))
707 (lambda unrestricted fitsPredecessor : Nat .
708 (lambda unrestricted fitsInduction : (family DataBytesBuilderResult) .
709 (nat-eliminate
710 (lambda unrestricted current : Nat . (family DataBytesBuilderResult))
711 (constructor
712 DataBytesBuilderResult
713 DataBytesBuilderSucceeded
714 dataBytesBuilderEmpty
715 (dataBytesZeroTelemetry allocationLimit))
716 (lambda unrestricted nonemptyPredecessor : Nat .
717 (lambda unrestricted nonemptyInduction : (family DataBytesBuilderResult) .
718 (constructor
719 DataBytesBuilderResult
720 DataBytesBuilderSucceeded
721 (constructor
722 DataBytesBuilder
723 DataBytesBuilderValue
724 (bytes-builder-chunk chunk)
725 chunkLength
726 dataBytesNaturalOne
727 chunkLength
728 zero)
729 (dataBytesTelemetry
730 chunkLength
731 chunkLength
732 zero
733 dataBytesNaturalOne
734 chunkLength
735 zero
736 zero
737 allocationLimit))))
738 chunkLength)))
739 (naturalLessOrEqual chunkLength allocationLimit)))
740 (bytes-length chunk))))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.