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