def checked_offset

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

import Base
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
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
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle

205def checked_offset(+depth: Nat, +length: Nat, +index: U32,
206  checked: {Storage.index_matches(depth, length, index) == True{} : Bool}) ->
207  {Model.offset(depth, Refinement.route(depth, index)) == U32.to_nat(index) : Nat}:
208  Lifecycle.natural_equal(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index),
209    Equal.sym(Bool, Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)), True{},
210      and_true_left(Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)),
211        Nat.is_lt(Model.offset(depth, Refinement.route(depth, index)), length), checked)))