487def embeddingGatherF32PlanFor =
488 (lambda unrestricted width : (family EmbeddingGatherF32Width) .
489 (lambda unrestricted tokenCount : Nat .
490 (nat-eliminate
491 (lambda unrestricted tokenCountNonzero : Nat . (family EmbeddingGatherF32PlanResult))
492 (constructor
493 EmbeddingGatherF32PlanResult
494 EmbeddingGatherF32PlanFailed
495 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32TokenCountZero)
496 (embeddingGatherF32RejectedTelemetry
497 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32TokenCountZero)
498 zero))
499 (lambda unrestricted nonzeroPredecessor : Nat .
500 (lambda unrestricted nonzeroInduction : (family EmbeddingGatherF32PlanResult) .
501 (app
502 (lambda unrestricted actualInstructions : Nat .
503 (nat-eliminate
504 (lambda unrestricted countValid : Nat . (family EmbeddingGatherF32PlanResult))
505 (constructor
506 EmbeddingGatherF32PlanResult
507 EmbeddingGatherF32PlanFailed
508 (constructor
509 EmbeddingGatherF32FailureCode
510 EmbeddingGatherF32InstructionCountMismatch)
511 (embeddingGatherF32RejectedTelemetry
512 (constructor
513 EmbeddingGatherF32FailureCode
514 EmbeddingGatherF32InstructionCountMismatch)
515 actualInstructions))
516 (lambda unrestricted countPredecessor : Nat .
517 (lambda unrestricted countInduction : (family EmbeddingGatherF32PlanResult) .
518 (constructor
519 EmbeddingGatherF32PlanResult
520 EmbeddingGatherF32PlanReady
521 (constructor
522 EmbeddingGatherF32Plan
523 EmbeddingGatherF32PlanValue
524 tokenCount
525 (embeddingGatherF32ProgramFor width)
526 (constructor
527 EmbeddingGatherF32Telemetry
528 EmbeddingGatherF32TelemetryValue
529 embeddingGatherF32NaturalTwenty
530 actualInstructions
531 embeddingGatherF32NaturalTwentyFour
532 tokenCount
533 tokenCount
534 (embeddingGatherF32BlockXFor width)
535 (embeddingGatherF32WidthElements width)
536 embeddingGatherF32NaturalTwelveThousandTwoHundredEightyEight
537 embeddingGatherF32NaturalFour
538 embeddingGatherF32NaturalFour
539 zero
540 zero
541 zero
542 zero)))))
543 (naturalEqual actualInstructions embeddingGatherF32NaturalTwenty)))
544 (sm86ProgramCount (embeddingGatherF32ProgramFor width)))))
545 (naturalNonzero tokenCount))))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.