def read_keeps

bendtorch-core@0.1.0.0 · src/tensor/reduction.bend:104

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

104# The array a read hands back is the array it read.
105def read_keeps(-depth: Nat, -original: Array<F32>, -balanced: Model.Balanced(F32, depth, original), -array: Array<F32>,
106  -index: U32, -pair: Array<F32> & F32, -exact: {pair == Array.get(F32, array, index) : Array<F32> & F32},
107  -same: {array == original : Array<F32>}) -> Fact<{array_from(pair) == original : Array<F32>}>:
108  Fact{Equal.trans(Array<F32>, array_from(pair), array_from(Array.get(F32, array, index)), original,
109    Equal.cong(Array<F32> & F32, Array<F32>, p => array_from(p), pair, Array.get(F32, array, index), exact),
110    Equal.trans(Array<F32>, array_from(Array.get(F32, array, index)), array, original,
111      Refinement.law_get_retains(F32, depth, array, index,
112        {\{Fact: p => p} : Fact<(Model.Balanced(F32, depth, array))> -> Model.Balanced(F32, depth, array)}(
113          kept_balanced(depth, original, balanced, array, same))),
114      same))}