547def sm86PlaceWord24Field =
548 (lambda unrestricted position : Nat .
549 (lambda unrestricted byte0 : Byte .
550 (lambda unrestricted byte1 : Byte .
551 (lambda unrestricted byte2 : Byte .
552 (lambda unrestricted encoded : Bytes .
553 (app
554 (nat-eliminate
555 (lambda unrestricted condition : Nat .
556 (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)))
557 (lambda unrestricted ignored : Nat .
558 (sm86FieldFailure
559 (constructor SM86EncodingErrorCode SM86EncodingWordLengthInvalid)
560 position
561 sm86EncodingNaturalTwentyFour
562 (bytes-length encoded)
563 (bytes-length encoded)))
564 (lambda unrestricted predecessor : Nat .
565 (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)) .
566 (lambda unrestricted ignored : Nat .
567 (sm86PlaceWord24FieldWithValidWord position byte0 byte1 byte2 encoded))))
568 (naturalEqual (bytes-length encoded) sm86EncodingNaturalSixteen))
569 zero))))))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.