481def indexedRowScatterSM86DestinationIndex =
482 (lambda unrestricted geometry : (family IndexedRowScatterSM86Geometry) .
483 (lambda unrestricted classId : Nat .
484 (lambda unrestricted component : Nat .
485 (nat-eliminate
486 (lambda unrestricted classIdInBounds : Nat . (family IndexedRowScatterSM86IndexResult))
487 (constructor
488 IndexedRowScatterSM86IndexResult
489 IndexedRowScatterIndexInvalid
490 (constructor IndexedRowScatterSM86FailureCode IndexedRowScatterClassIdOutOfBounds)
491 classId
492 component)
493 (lambda unrestricted classIdPredecessor : Nat .
494 (lambda unrestricted classIdInduction : (family IndexedRowScatterSM86IndexResult) .
495 (nat-eliminate
496 (lambda unrestricted componentInBounds : Nat .
497 (family IndexedRowScatterSM86IndexResult))
498 (constructor
499 IndexedRowScatterSM86IndexResult
500 IndexedRowScatterIndexInvalid
501 (constructor
502 IndexedRowScatterSM86FailureCode
503 IndexedRowScatterDestinationComponentOutOfBounds)
504 classId
505 component)
506 (lambda unrestricted componentPredecessor : Nat .
507 (lambda unrestricted componentInduction : (family IndexedRowScatterSM86IndexResult) .
508 (constructor
509 IndexedRowScatterSM86IndexResult
510 IndexedRowScatterIndexValid
511 (naturalAdd
512 (naturalMultiply classId (indexedRowScatterSM86WidthNatural geometry))
513 component))))
514 (naturalLess component (indexedRowScatterSM86WidthNatural geometry)))))
515 (naturalLess classId indexedRowScatterSM86N12288)))))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.