445def indexedRowScatterSM86SourceIndex =
446 (lambda unrestricted geometry : (family IndexedRowScatterSM86Geometry) .
447 (lambda unrestricted row : Nat .
448 (lambda unrestricted component : Nat .
449 (nat-eliminate
450 (lambda unrestricted rowInBounds : Nat . (family IndexedRowScatterSM86IndexResult))
451 (constructor
452 IndexedRowScatterSM86IndexResult
453 IndexedRowScatterIndexInvalid
454 (constructor IndexedRowScatterSM86FailureCode IndexedRowScatterSourceRowOutOfBounds)
455 row
456 component)
457 (lambda unrestricted rowPredecessor : Nat .
458 (lambda unrestricted rowInduction : (family IndexedRowScatterSM86IndexResult) .
459 (nat-eliminate
460 (lambda unrestricted componentInBounds : Nat .
461 (family IndexedRowScatterSM86IndexResult))
462 (constructor
463 IndexedRowScatterSM86IndexResult
464 IndexedRowScatterIndexInvalid
465 (constructor
466 IndexedRowScatterSM86FailureCode
467 IndexedRowScatterSourceComponentOutOfBounds)
468 row
469 component)
470 (lambda unrestricted componentPredecessor : Nat .
471 (lambda unrestricted componentInduction : (family IndexedRowScatterSM86IndexResult) .
472 (constructor
473 IndexedRowScatterSM86IndexResult
474 IndexedRowScatterIndexValid
475 (naturalAdd
476 (naturalMultiply row (indexedRowScatterSM86WidthNatural geometry))
477 component))))
478 (naturalLess component (indexedRowScatterSM86WidthNatural geometry)))))
479 (naturalLess row (indexedRowScatterSM86RowsNatural geometry))))))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.