448def embeddingGatherF32Offset =
449 (lambda unrestricted token : Nat .
450 (lambda unrestricted channel : Nat .
451 (nat-eliminate
452 (lambda unrestricted tokenValid : Nat . (family EmbeddingGatherF32OffsetResult))
453 (constructor
454 EmbeddingGatherF32OffsetResult
455 EmbeddingGatherF32OffsetInvalid
456 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32TokenOutOfBounds)
457 token
458 channel)
459 (lambda unrestricted tokenPredecessor : Nat .
460 (lambda unrestricted tokenInduction : (family EmbeddingGatherF32OffsetResult) .
461 (nat-eliminate
462 (lambda unrestricted channelValid : Nat . (family EmbeddingGatherF32OffsetResult))
463 (constructor
464 EmbeddingGatherF32OffsetResult
465 EmbeddingGatherF32OffsetInvalid
466 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32ChannelOutOfBounds)
467 token
468 channel)
469 (lambda unrestricted channelPredecessor : Nat .
470 (lambda unrestricted channelInduction : (family EmbeddingGatherF32OffsetResult) .
471 (constructor
472 EmbeddingGatherF32OffsetResult
473 EmbeddingGatherF32OffsetValid
474 (naturalMultiply
475 embeddingGatherF32NaturalFour
476 (naturalAdd
477 (naturalMultiply token embeddingGatherF32NaturalOneThousandTwentyFour)
478 channel)))))
479 (naturalLess channel embeddingGatherF32NaturalOneThousandTwentyFour))))
480 (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.