def Reads

bendtorch-core@0.1.0.0 · src/autograd/reduce_parallel_proof.bend:748

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws

748# The words a walk saw are the contribution's words at the offsets it read.
749def Reads(+d: Nat, -A: Array<F32>, +values: List<&2, F32>, +bound: Nat) -> Type:
750  @+position: Nat -> @inside: {Nat.is_lt(position, bound) == True{} : Bool} ->
751    {Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(position))) == ReduceLaws.word_at(values, position) : Maybe<&2, F32>}