def position_step

bendtorch-core@0.1.0.0 · src/tensor/contracts/build_facts.bend:115

import Base
import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

115def position_step(+capacity: Nat, +offset: Nat, +base: Nat) ->
116  {Nat.add(offset, Nat.add(capacity, base)) == Nat.add(Nat.add(capacity, offset), base) : Nat}:
117  Equal.trans(Nat, Nat.add(offset, Nat.add(capacity, base)), Nat.add(capacity, Nat.add(offset, base)), Nat.add(Nat.add(capacity, offset), base),
118    Nats.add_swap(offset, capacity, base), Index.add_assoc(capacity, offset, base))