def eta

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:507

import Base
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallel

507# The facts of `ReduceParallel.fast_fiber`, stated for the replayed arrays
508# `Api.arr`, which a proof can name as often as it needs: a read of
509# `Api.arr(h, d, f)` hands back that array, next to the word it read.
510def eta(pair: Array<F32> & F32) -> {pair == (Refinement.first(F32, pair), Refinement.second(F32, pair)) : Array<F32> & F32}:
511  match pair:
512    case Tuple{x, y}:
513      {==}