571def sm86PlaceEncodedField =
572 (lambda unrestricted field : (family SM86EncodedField) .
573 (lambda unrestricted encoded : Bytes .
574 (eliminate
575 SM86EncodedField
576 (lambda unrestricted current : (family SM86EncodedField) . (family SM86FieldEncodingResult))
577 field
578 (branch
579 SM86EncodedFieldValue
580 position
581 width
582 value
583 .
584 (app
585 (lambda unrestricted extent : Nat .
586 (nat-eliminate
587 (lambda unrestricted wordLengthValid : Nat . (family SM86FieldEncodingResult))
588 (sm86FieldFailure
589 (constructor SM86EncodingErrorCode SM86EncodingWordLengthInvalid)
590 position
591 width
592 (bytes-length encoded)
593 (bytes-length encoded))
594 (lambda unrestricted lengthPredecessor : Nat .
595 (lambda unrestricted lengthInduction : (family SM86FieldEncodingResult) .
596 (nat-eliminate
597 (lambda unrestricted widthValid : Nat . (family SM86FieldEncodingResult))
598 (sm86FieldFailure
599 (constructor SM86EncodingErrorCode SM86EncodingFieldWidthInvalid)
600 position
601 width
602 width
603 (bytes-length encoded))
604 (lambda unrestricted widthPredecessor : Nat .
605 (lambda unrestricted widthInduction : (family SM86FieldEncodingResult) .
606 (nat-eliminate
607 (lambda unrestricted extentValid : Nat .
608 (family SM86FieldEncodingResult))
609 (sm86FieldFailure
610 (constructor SM86EncodingErrorCode SM86EncodingFieldExtentInvalid)
611 position
612 width
613 extent
614 (bytes-length encoded))
615 (lambda unrestricted extentPredecessor : Nat .
616 (lambda unrestricted extentInduction : (family SM86FieldEncodingResult) .
617 (nat-eliminate
618 (lambda unrestricted valueValid : Nat .
619 (family SM86FieldEncodingResult))
620 (sm86FieldFailure
621 (constructor
622 SM86EncodingErrorCode
623 SM86EncodingFieldValueOverflow)
624 position
625 width
626 value
627 (bytes-length encoded))
628 (lambda unrestricted valuePredecessor : Nat .
629 (lambda unrestricted valueInduction : (family SM86FieldEncodingResult) .
630 (constructor
631 SM86FieldEncodingResult
632 SM86FieldEncodingSucceeded
633 (sm86PlaceFieldBitsUnchecked position width value encoded)
634 (sm86FieldTelemetryOne width extent))))
635 (sm86FieldValueFits width value))))
636 (naturalLessOrEqual extent sm86EncodingNaturalOneHundredTwentyEight))))
637 (nat-less-than zero width))))
638 (naturalEqual (bytes-length encoded) sm86EncodingNaturalSixteen)))
639 (naturalAdd position width)))
640 (branch
641 SM86EncodedFieldWord32Value
642 position
643 value
644 .
645 (sm86PlaceWord32Field position value encoded))
646 (branch
647 SM86EncodedFieldWord24Value
648 position
649 byte0
650 byte1
651 byte2
652 .
653 (sm86PlaceWord24Field position byte0 byte1 byte2 encoded)))))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.