CorePROOF.natural_decision_certificate: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
Lines 651-659 of bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&start_line=651&end_line=659

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

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

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=output_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=converted_step_certificate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=step_certificate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=ConvertedCertificate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=NaturalStep
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=State