~/jendhub

def natural_decision_certificate

bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:651

import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

651def natural_decision_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat, +index: U32,
652  decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>, state: Elementwise.State<Shape.output_shape(plan)>) ->
653  Elementwise.ConvertedCertificate<operation, plan, cursor, index, decision, state>:
654  match decision:
655    case Shape.BFalse{equal}:
656      Elementwise.State{left, right, output} = state
657      Elementwise.ConvertedCertificate{Elementwise.NaturalStop{left, right, Core.StorageError{Storage.InvalidIndex{}}}, {==}, Unit{}}
658    case Shape.BTrue{+equal}:
659      converted_step_certificate(operation, plan, cursor, index, equal, state, step_certificate(operation, plan, index, state))

Uses (16)

Used by (1)