def got

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

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

515def got(+h: List<&2, Api.Effect>, +d: Nat, +f: F32, +i: U32) ->
516  {Array.get(F32, Api.arr(h, d, f), i) == (Api.arr(h, d, f), Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), i))) : Array<F32> & F32}:
517  Equal.trans(Array<F32> & F32, Array.get(F32, Api.arr(h, d, f), i),
518    (Refinement.first(F32, Array.get(F32, Api.arr(h, d, f), i)), Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), i))),
519    (Api.arr(h, d, f), Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), i))),
520    eta(Array.get(F32, Api.arr(h, d, f), i)),
521    Equal.cong(Array<F32>, Array<F32> & F32, a => (a, Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), i))),
522      Refinement.first(F32, Array.get(F32, Api.arr(h, d, f), i)), Api.arr(h, d, f),
523      Refinement.law_get_retains(F32, d, Api.arr(h, d, f), i, Api.bal(h, d, f))))