def read_original

bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:356

import Base
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core

356def read_original(-original: Core.Dynamic, -owner: Core.Dynamic, +index: U32, same: {owner == original : Core.Dynamic},
357  certificate: Core.DynamicRead<owner, index>) -> Core.DynamicRead<original, index>:
358  Core.DynamicRead{dynamic, result, exact} = certificate
359  Core.DynamicRead{dynamic, result, Equal.trans(Core.Dynamic & Result<&2, &2, Core.Error, F32>, (dynamic, result),
360    Core.read_dynamic(owner, index), Core.read_dynamic(original, index), exact,
361    Equal.cong(Core.Dynamic, Core.Dynamic & Result<&2, &2, Core.Error, F32>, input => Core.read_dynamic(input, index), owner, original, same))}