Parallel.Certified: type of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Parallel
Lines 86-91 of bendtorch-core@0.1.0.0/src/tensor/parallel.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&start_line=86&end_line=91

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

# A run of the one-thread tree next to its proof of balance: `result` is
# the term the code computes, and its first component is balanced at
# `depth`. The proofs only follow the code, so they cost nothing at runtime.
type Certified<-S: Type, -depth: Nat, -expected: Array<F32> & S> is Type:
  Certified{result: Array<F32> & S, same: {result == expected : Array<F32> & S},
    balanced: Model.Balanced(F32, depth, Pair.fst(Array<F32>, S, result))}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced