457def embeddingGatherF32Offset =
458 (lambda unrestricted token : Nat .
459 (lambda unrestricted channel : Nat .
460 (nat-eliminate
461 (lambda unrestricted tokenValid : Nat . (family EmbeddingGatherF32OffsetResult))
462 (constructor
463 EmbeddingGatherF32OffsetResult
464 EmbeddingGatherF32OffsetInvalid
465 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32TokenOutOfBounds)
466 token
467 channel)
468 (lambda unrestricted tokenPredecessor : Nat .
469 (lambda unrestricted tokenInduction : (family EmbeddingGatherF32OffsetResult) .
470 (nat-eliminate
471 (lambda unrestricted channelValid : Nat . (family EmbeddingGatherF32OffsetResult))
472 (constructor
473 EmbeddingGatherF32OffsetResult
474 EmbeddingGatherF32OffsetInvalid
475 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32ChannelOutOfBounds)
476 token
477 channel)
478 (lambda unrestricted channelPredecessor : Nat .
479 (lambda unrestricted channelInduction : (family EmbeddingGatherF32OffsetResult) .
480 (constructor
481 EmbeddingGatherF32OffsetResult
482 EmbeddingGatherF32OffsetValid
483 (naturalMultiply
484 embeddingGatherF32NaturalFour
485 (naturalAdd
486 (naturalMultiply token embeddingGatherF32NaturalOneThousandTwentyFour)
487 channel)))))
488 (naturalLess channel embeddingGatherF32NaturalOneThousandTwentyFour))))
489 (naturalLess token embeddingGatherF32NaturalTwelveThousandTwoHundredEightyEight))))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.