def SourceReads

bendtorch-core@0.1.0.0 · src/tensor/elementwise_parallel_proof.bend:244

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
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/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality

244# What `take` hands back for one input: the copy for the build is balanced at
245# some depth and, below the input's element count, holds what the checked
246# observation of the input sees; the kept tensor observes like the input.
247def SourceReads(-input: Core.Dynamic, -depth: Nat, -copy: Array<F32>) -> Type:
248  @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Totality.dimensions(input))) == True{} : Bool} ->
249    {Model.observe(F32, depth, copy, Refinement.route(depth, index)) == Core.checked_observe_dynamic(input, index) : Maybe<&2, F32>}