472def sm86PlaceWord32Field =
473 (lambda unrestricted position : Nat .
474 (lambda unrestricted value : (family SM86Unsigned32) .
475 (lambda unrestricted encoded : Bytes .
476 (app
477 (nat-eliminate
478 (lambda unrestricted current : Nat .
479 (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)))
480 (lambda unrestricted ignored : Nat .
481 (sm86FieldFailure
482 (constructor SM86EncodingErrorCode SM86EncodingWordLengthInvalid)
483 position
484 sm86EncodingNaturalThirtyTwo
485 (bytes-length encoded)
486 (bytes-length encoded)))
487 (lambda unrestricted predecessor : Nat .
488 (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family SM86FieldEncodingResult)) .
489 (lambda unrestricted ignored : Nat .
490 (sm86PlaceWord32FieldWithValidWord position value encoded))))
491 (naturalEqual (bytes-length encoded) sm86EncodingNaturalSixteen))
492 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.